diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 40dc275d9..1fab85e0c 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -539,14 +539,16 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
Dom.Summary.pp_summary s
let checker : Callbacks.proc_callback_args -> Specs.summary
- = fun ({ summary } as callback) ->
+ = fun ({ proc_desc; tenv; summary } as callback) ->
let proc_name = Specs.get_proc_name summary in
let make_extras _ = callback.get_proc_desc in
let updated_summary : Specs.summary =
- Interprocedural.compute_and_store_post
+ Interprocedural.compute_summary
~compute_post
~make_extras
- callback in
+ proc_desc
+ tenv
+ summary in
let post =
updated_summary.payload.buffer_overrun in
begin
diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml
index 282dddb29..4e4625532 100644
--- a/infer/src/checkers/AbstractInterpreter.ml
+++ b/infer/src/checkers/AbstractInterpreter.ml
@@ -157,14 +157,12 @@ end
module Interprocedural (Summ : Summary.S) = struct
- let compute_and_store_post
- ~compute_post ~make_extras { Callbacks.proc_desc; summary; tenv; } : Specs.summary =
+ let compute_summary ~compute_post ~make_extras proc_desc tenv summary =
match compute_post (ProcData.make proc_desc tenv (make_extras proc_desc)) with
| Some post ->
Summ.update_summary post summary
| None ->
summary
-
end
module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) =
diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli
index 89fbaa97b..bf0c8794f 100644
--- a/infer/src/checkers/AbstractInterpreter.mli
+++ b/infer/src/checkers/AbstractInterpreter.mli
@@ -67,11 +67,13 @@ module Make
(** create an interprocedural abstract interpreter given logic for handling summaries *)
module Interprocedural (Summary : Summary.S) : sig
- (** compute and return the summary for the given procedure and store it on disk using
- [compute_post]. *)
- val compute_and_store_post :
+ (** compute a summary for the given procedure using [compute_post] and write it into the
+ aggregated [Specs.summary] *)
+ val compute_summary :
compute_post: ('a ProcData.t -> Summary.payload option) ->
make_extras : (Procdesc.t -> 'a) ->
- Callbacks.proc_callback_args ->
+ Procdesc.t ->
+ Tenv.t ->
+ Specs.summary ->
Specs.summary
end
diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml
index 67d99761a..33af84b1d 100644
--- a/infer/src/checkers/NullabilitySuggest.ml
+++ b/infer/src/checkers/NullabilitySuggest.ml
@@ -164,7 +164,7 @@ let pretty_field_name proc_data field_name =
(* This format is subject to change once this checker gets to run on C/Cpp/ObjC *)
Fieldname.to_string field_name
-let checker ({ Callbacks.summary } as callback) =
+let checker { Callbacks.summary; proc_desc; tenv; } =
let report astate (proc_data : extras ProcData.t) =
let report_access_path ap udchain =
let issue_kind = Localise.to_issue_id Localise.field_should_be_nullable in
@@ -199,4 +199,4 @@ let checker ({ Callbacks.summary } as callback) =
"Analyzer failed to compute post for %a"
Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc)
in
- Interprocedural.compute_and_store_post ~compute_post ~make_extras:(fun _ -> ()) callback
+ Interprocedural.compute_summary ~compute_post ~make_extras:(fun _ -> ()) proc_desc tenv summary
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index cd4fb2691..484f5bb43 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -244,12 +244,14 @@ let compute_post proc_data =
~initial:(SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty)
|> Option.map ~f:SiofDomain.normalize
-let checker ({ Callbacks.proc_desc } as callback) : Specs.summary =
+let checker { Callbacks.proc_desc; tenv; summary } : Specs.summary =
let updated_summary =
- Interprocedural.compute_and_store_post
+ Interprocedural.compute_summary
~compute_post
~make_extras:ProcData.make_empty_extras
- callback in
+ proc_desc
+ tenv
+ summary in
let pname = Procdesc.get_proc_name proc_desc in
begin
match Typ.Procname.get_global_name_of_initializer pname with
diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index 48350eea6..391277f6c 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -866,7 +866,7 @@ let empty_post =
and return_attrs = ThreadSafetyDomain.AttributeSetDomain.empty in
(initial_thumbs_up, initial_known_on_ui_thread, has_lock, ThreadSafetyDomain.AccessDomain.empty, return_attrs)
-let analyze_procedure callback =
+let analyze_procedure { Callbacks.proc_desc; tenv; summary; } =
let is_initializer tenv proc_name =
Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
let open ThreadSafetyDomain in
@@ -917,10 +917,7 @@ let analyze_procedure callback =
end
else
Some empty_post in
- Interprocedural.compute_and_store_post
- ~compute_post
- ~make_extras:FormalMap.make
- callback
+ Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary
(* we assume two access paths can alias if their access parts are equal (we ignore the base). *)
let can_alias access_path1 access_path2 =
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index 4e16a0e48..192b11786 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -392,24 +392,26 @@ let check_expensive_subtyping_rules { Callbacks.proc_desc; tenv; summary } overr
module Interprocedural = struct
include AbstractInterpreter.Interprocedural(Summary)
- let check_and_report ({ Callbacks.proc_desc; tenv } as proc_data) : Specs.summary =
+ let check_and_report ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
let proc_name = Procdesc.get_proc_name proc_desc in
if is_expensive tenv proc_name then
- PatternMatch.override_iter (check_expensive_subtyping_rules proc_data) tenv proc_name;
+ PatternMatch.override_iter (check_expensive_subtyping_rules callback) tenv proc_name;
let initial =
(AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in
let compute_post proc_data =
Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in
let updated_summary : Specs.summary =
- compute_and_store_post
+ compute_summary
~compute_post:compute_post
~make_extras:ProcData.make_empty_extras
- proc_data in
+ proc_desc
+ tenv
+ summary in
begin
match updated_summary.payload.annot_map with
| Some annot_map ->
- List.iter ~f:(report_src_snk_paths proc_data annot_map) src_snk_pairs
+ List.iter ~f:(report_src_snk_paths callback annot_map) src_snk_pairs
| None ->
()
end;
diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml
index 39e09059d..46d0a0eb0 100644
--- a/infer/src/labs/ResourceLeaks.ml
+++ b/infer/src/labs/ResourceLeaks.ml
@@ -97,7 +97,7 @@ module Analyzer =
module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
(* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
-let checker ({ Callbacks.summary; } as callback) : Specs.summary =
+let checker { Callbacks.summary; proc_desc; tenv; } : Specs.summary =
(* Report an error when we have acquired more resources than we have released *)
let report leak_count (proc_data : extras ProcData.t) =
if leak_count > 0 (* 3(a) *)
@@ -123,4 +123,4 @@ let checker ({ Callbacks.summary; } as callback) : Specs.summary =
"Analyzer failed to compute post for %a"
Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) in
- Interprocedural.compute_and_store_post ~compute_post ~make_extras:FormalMap.make callback
+ Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 645f8c22f..c0e76ce78 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -614,7 +614,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
- let checker ({ Callbacks.tenv; summary; } as callback) : Specs.summary =
+ let checker { Callbacks.tenv; summary; proc_desc; } : Specs.summary =
(* bind parameters to a trace with a tainted source (if applicable) *)
let make_initial pdesc =
@@ -650,5 +650,5 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let make_extras pdesc =
let formal_map = FormalMap.make pdesc in
{ formal_map; summary; } in
- Interprocedural.compute_and_store_post ~compute_post ~make_extras callback
+ Interprocedural.compute_summary ~compute_post ~make_extras proc_desc tenv summary
end