diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index d0a971f7e..828978a16 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -638,28 +638,33 @@ let get_local_decls proc_desc = let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = fun {proc_desc; tenv; integer_type_widths; summary} -> Preanal.do_preanalysis proc_desc tenv ; - let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in - let pdata = ProcData.make proc_desc tenv oenv in + let pdata = + let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in + ProcData.make proc_desc tenv oenv + in let cfg = CFG.from_pdesc proc_desc in let initial = Init.initial_state pdata (CFG.start_node cfg) in let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in - let locals = get_local_decls proc_desc in - let exit_mem = - extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map - |> Option.map ~f:(Dom.Mem.forget_locs locals) - in - let cond_set = - Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map - |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary - in + let exit_node = CFG.exit_node cfg in + let underlying_exit_node = CFG.Node.underlying_node exit_node in + let pp_name f = F.pp_print_string f "bufferoverrun check" in + NodePrinter.start_session ~pp_name underlying_exit_node ; let summary = + let locals = get_local_decls proc_desc in + let cond_set = + Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map + |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary + in + let exit_mem = extract_post (CFG.Node.id exit_node) inv_map in match exit_mem with | Some exit_mem -> - let post = (Dom.Mem.unset_oenv exit_mem, cond_set) in - Payload.update_summary post summary + let exit_mem = exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv in + let payload = (exit_mem, cond_set) in + Payload.update_summary payload summary | _ -> summary in + NodePrinter.finish_session underlying_exit_node ; if Config.hoisting_report_only_expensive then let pname = Procdesc.get_proc_name proc_desc in WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index cf1be2000..959d5f90b 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -343,12 +343,11 @@ let rec eval_sympath_partial params p mem = match p with | Symb.SymbolPath.Pvar x -> ( try ParamBindings.find x params with Caml.Not_found -> - L.(debug BufferOverrun Verbose) - "Symbol %a is not found in parameters.@\n" (Pvar.pp Pp.text) x ; + L.d_printfln "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ; Val.Itv.top ) | Symb.SymbolPath.Callsite {cs} -> - L.(debug BufferOverrun Verbose) - "Symbol for %a is not expected to be in parameters.@\n" Typ.Procname.pp (CallSite.pname cs) ; + L.d_printfln "Symbol for %a is not expected to be in parameters." Typ.Procname.pp + (CallSite.pname cs) ; Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ -> let locs = eval_locpath params p mem in @@ -369,8 +368,7 @@ and eval_locpath params p mem = PowLoc.append_field ~fn locs in if PowLoc.is_empty res then ( - L.(debug BufferOverrun Verbose) - "Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ; + L.d_printfln "Location value for %a is not found." Symb.SymbolPath.pp_partial p ; PowLoc.unknown ) else res