From bfcc88a5e2ee82310411977b93f7c471ce5b67fb Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 25 May 2018 08:20:44 -0700 Subject: [PATCH] Inferbo: use instr_is_auxiliary Reviewed By: jvillard Differential Revision: D8160995 fbshipit-source-id: 99190a9 --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 42888039b..a0a6bf2f8 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -315,19 +315,12 @@ module Report = struct module PO = BufferOverrunProofObligations module ExitStatement = struct - let non_significant_instr = function - | Sil.(Abstract _ | Nullify _ | Remove_temps _) -> - true - | _ -> - false - - (* check that we are the last significant instruction * of a procedure (no more significant instruction) * or of a block (goes directly to a node with multiple predecessors) *) let rec is_end_of_block_or_procedure (cfg: CFG.t) node rem_instrs = - List.for_all rem_instrs ~f:non_significant_instr + List.for_all rem_instrs ~f:Sil.instr_is_auxiliary && match CFG.succs cfg node with | [] ->