diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 285bad5d2..25f48aaa6 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1467,7 +1467,8 @@ let do_analysis exe_env = let summaryre = Config.run_in_re_execution_mode (analyze_proc source exe_env) proc_desc in - Specs.add_summary proc_name summaryre in + Specs.add_summary proc_name summaryre; + summaryre in { Ondemand.analyze_ondemand; get_proc_desc; diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 311094d39..334cf62dc 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -27,7 +27,7 @@ let dirs_to_analyze = changed_files String.Set.empty in Option.map ~f:process_changed_files SourceFile.changed_files_set -type analyze_ondemand = SourceFile.t -> Procdesc.t -> unit +type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary type get_proc_desc = Procname.t -> Procdesc.t option @@ -141,9 +141,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc Specs.set_status callee_pname Specs.Active; source in - let postprocess source = + let postprocess source summary = decr nesting; - let summary = Specs.get_summary_unsafe "ondemand" callee_pname in Specs.store_summary callee_pname summary; Printer.write_proc_html source false callee_pdesc; summary in @@ -161,8 +160,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc let old_state = save_global_state () in let source = preprocess () in try - analyze_proc source callee_pdesc; - let summary = postprocess source in + let summary = + analyze_proc source callee_pdesc |> postprocess source in restore_global_state old_state; summary with exn -> diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index deea928d3..1a2a7076b 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -15,7 +15,7 @@ open! IStd will be analyzed *) val dirs_to_analyze : String.Set.t option -type analyze_ondemand = SourceFile.t -> Procdesc.t -> unit +type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary type get_proc_desc = Procname.t -> Procdesc.t option diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 568df121c..fc4c0bd76 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -168,7 +168,10 @@ module Interprocedural (Summ : Summary.S) = struct | None -> None in let analyze_ondemand source pdesc = - ignore (analyze_ondemand_ source pdesc) in + ignore (analyze_ondemand_ source pdesc); + Specs.get_summary_unsafe + "Inferprocedural.compute_and_store_post" + (Procdesc.get_proc_name pdesc) in let callbacks = { Ondemand.analyze_ondemand; diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 924f6e82b..aac868cd6 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -414,7 +414,8 @@ let callback_eradicate { callback_args with Callbacks.idenv = idenv_pname; proc_name = (Procdesc.get_proc_name pdesc); - proc_desc = pdesc; } in + proc_desc = pdesc; }; + Specs.get_summary_unsafe "callback_eradicate" (Procdesc.get_proc_name pdesc) in { Ondemand.analyze_ondemand; get_proc_desc;