diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index db697681d..1aa9cd9dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -262,7 +262,7 @@ type get_checks_summary = Procname.t -> checks_summary option let check_instr : get_checks_summary -> BoUtils.get_formals - -> Procdesc.t + -> Procname.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.Node.t @@ -270,7 +270,7 @@ let check_instr : -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t = - fun get_checks_summary get_formals pdesc tenv integer_type_widths node instr mem cond_set -> + fun get_checks_summary get_formals pname tenv integer_type_widths node instr mem cond_set -> match instr with | Sil.Load {e= exp; loc= location} -> cond_set @@ -295,7 +295,6 @@ let check_instr : | Some {Models.check} -> let model_env = let node_hash = CFG.Node.hash node in - let pname = Procdesc.get_proc_name pdesc in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths in check model_env mem cond_set @@ -329,7 +328,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un let check_instrs : get_checks_summary -> BoUtils.get_formals - -> Procdesc.t + -> Procname.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t @@ -338,7 +337,7 @@ let check_instrs : -> Dom.Mem.t AbstractInterpreter.State.t -> Checks.t -> Checks.t = - fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs state checks -> + fun get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs state checks -> match state with | _ when Instrs.is_empty instrs -> checks @@ -355,7 +354,7 @@ let check_instrs : checks in let cond_set = - check_instr get_checks_summary get_formals pdesc tenv integer_type_widths node instr pre + check_instr get_checks_summary get_formals pname tenv integer_type_widths node instr pre checks.cond_set in print_debug_info instr pre cond_set ; @@ -365,7 +364,7 @@ let check_instrs : let check_node : get_checks_summary -> BoUtils.get_formals - -> Procdesc.t + -> Procname.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t @@ -373,11 +372,11 @@ let check_node : -> Checks.t -> CFG.Node.t -> Checks.t = - fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map checks node -> + fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map checks node -> match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with | Some state -> let instrs = CFG.instrs node in - check_instrs get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs + check_instrs get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs state checks | _ -> checks @@ -388,15 +387,15 @@ type checks = Checks.t let compute_checks : get_checks_summary -> BoUtils.get_formals - -> Procdesc.t + -> Procname.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> BufferOverrunAnalysis.invariant_map -> checks = - fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map -> + fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map -> CFG.fold_nodes cfg - ~f:(check_node get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map) + ~f:(check_node get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map) ~init:Checks.empty @@ -443,7 +442,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t = let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals in - compute_checks get_checks_summary get_formals proc_desc tenv integer_type_widths cfg inv_map + compute_checks get_checks_summary get_formals proc_name tenv integer_type_widths cfg inv_map in report_errors tenv checks summary ; let cond_set = get_checks_summary checks in