diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 71ee041ed..8e4fedcf6 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -117,7 +117,7 @@ let restore_global_state st = let do_analysis ~propagate_exceptions curr_pdesc callee_pname = let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in - let really_do_analysis analyze_proc = + let really_do_analysis callee_pdesc analyze_proc = if trace () then L.stderr "[%d] really_do_analysis %a -> %a@." !nesting Procname.pp curr_pname @@ -150,7 +150,8 @@ let do_analysis ~propagate_exceptions curr_pdesc callee_pname = Specs.status = Specs.INACTIVE; timestamp = summary.Specs.timestamp + 1 } in Specs.add_summary callee_pname summary'; - Checkers.ST.store_summary callee_pname in + Checkers.ST.store_summary callee_pname; + Printer.proc_write_log false callee_pdesc in let log_error_and_continue exn kind = Reporting.log_error callee_pname exn; @@ -194,8 +195,10 @@ let do_analysis ~propagate_exceptions curr_pdesc callee_pname = when procedure_should_be_analyzed callee_pname -> begin match callbacks.get_proc_desc callee_pname with - | Some _ -> really_do_analysis callbacks.analyze_ondemand - | None -> () + | Some callee_pdesc -> + really_do_analysis callee_pdesc callbacks.analyze_ondemand + | None -> + () end | _ -> () (* skipping *) diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index e86f63ec7..f954c8ad2 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -258,9 +258,10 @@ let finish_session node = end (** Write log file for the proc *) -let _proc_write_log whole_seconds cfg pname = - match Cfg.Procdesc.find_from_name cfg pname with - | Some pdesc -> +let proc_write_log whole_seconds pdesc = + if !Config.write_html then + begin + let pname = Cfg.Procdesc.get_proc_name pdesc in let nodes = IList.sort Cfg.Node.compare (Cfg.Procdesc.get_nodes pdesc) in let linenum = (Cfg.Node.get_loc (IList.hd nodes)).Location.line in let fd, fmt = @@ -281,10 +282,7 @@ let _proc_write_log whole_seconds cfg pname = | Some summary -> Specs.pp_summary (pe_html Black) whole_seconds fmt summary; Io_infer.Html.close (fd, fmt)) - | None -> () - -let proc_write_log whole_seconds cfg pname = - if !Config.write_html then _proc_write_log whole_seconds cfg pname + end (** Creare a hash table mapping line numbers to the set of errors occurring on that line *) let create_errors_per_line err_log = diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 9309b9cc5..87f298eaf 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -29,7 +29,7 @@ val start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit val finish_session : Cfg.node -> unit (** Write log file for the proc, the boolean indicates whether to print whole seconds only *) -val proc_write_log : bool -> Cfg.cfg -> Procname.t -> unit +val proc_write_log : bool -> Cfg.Procdesc.t -> unit (** Module to read specific lines from files. The data from any file will stay in memory until the handle is collected by the gc *)