diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml
index 970f7693c..3eb98b3d7 100644
--- a/infer/src/backend/callbacks.ml
+++ b/infer/src/backend/callbacks.ml
@@ -18,11 +18,11 @@ type proc_callback_args = {
   get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
   idenv : Idenv.t;
   tenv : Tenv.t;
-  proc_name : Typ.Procname.t;
+  summary : Specs.summary;
   proc_desc : Procdesc.t;
 }
 
-type proc_callback_t = proc_callback_args -> unit
+type proc_callback_t = proc_callback_args -> Specs.summary
 
 type cluster_callback_t =
   Exe_env.t ->
@@ -58,13 +58,12 @@ let get_language proc_name = if Typ.Procname.is_java proc_name then Config.Java
 
 
 let reset_summary proc_name =
-  let should_reset =
-    is_none (Specs.get_summary proc_name) in
-  if should_reset
-  then
-    let attributes_opt =
-      Specs.proc_resolve_attributes proc_name in
-    Specs.reset_summary proc_name attributes_opt None
+  match Specs.get_summary proc_name with
+  | Some summary -> summary
+  | None ->
+      let attributes_opt =
+        Specs.proc_resolve_attributes proc_name in
+      Specs.reset_summary proc_name attributes_opt None
 
 
 (** Invoke all registered procedure callbacks on the given procedure. *)
@@ -82,39 +81,41 @@ let iterate_procedure_callbacks exe_env caller_pname =
     | None ->
         [] in
 
-  let update_time proc_name elapsed =
-    match Specs.get_summary proc_name with
-    | Some prev_summary ->
-        let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
-        let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
-        let summary = { prev_summary with Specs.stats = stats } in
-        Specs.add_summary proc_name summary
-    | None -> () in
-
-  Option.iter
-    ~f:(fun (idenv, tenv, proc_name, proc_desc, _) ->
-        List.iter
-          ~f:(fun (language_opt, proc_callback) ->
-              let language_matches = match language_opt with
-                | Some language -> Config.equal_language language procedure_language
-                | None -> true in
-              if language_matches then
-                begin
-                  let init_time = Unix.gettimeofday () in
-                  proc_callback
-                    {
-                      get_proc_desc;
-                      get_procs_in_file;
-                      idenv;
-                      tenv;
-                      proc_name;
-                      proc_desc;
-                    };
-                  let elapsed = Unix.gettimeofday () -. init_time in
-                  update_time proc_name elapsed
-                end)
-          !procedure_callbacks)
-    (get_procedure_definition exe_env caller_pname)
+  let update_time elapsed prev_summary =
+    let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
+    let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
+    let summary = { prev_summary with Specs.stats = stats } in
+    let proc_name = Specs.get_proc_name summary in
+    Specs.add_summary proc_name summary;
+    summary in
+
+  match get_procedure_definition exe_env caller_pname with
+  | None -> ()
+  | Some (idenv, tenv, proc_name, proc_desc, _) ->
+      ignore
+        (List.fold
+           ~init:(reset_summary proc_name)
+           ~f:(fun summary (language_opt, proc_callback) ->
+               let language_matches = match language_opt with
+                 | Some language -> Config.equal_language language procedure_language
+                 | None -> true in
+               if language_matches then
+                 let init_time = Unix.gettimeofday () in
+                 proc_callback
+                   {
+                     get_proc_desc;
+                     get_procs_in_file;
+                     idenv;
+                     tenv;
+                     summary;
+                     proc_desc;
+                   }
+                 |> update_time (Unix.gettimeofday () -. init_time)
+               else
+                 summary)
+           !procedure_callbacks);
+      Specs.store_summary (Specs.get_summary_unsafe "iterate_procedure_callbacks" proc_name)
+
 
 (** Invoke all registered cluster callbacks on a cluster of procedures. *)
 let iterate_cluster_callbacks all_procs exe_env proc_names =
@@ -151,7 +152,7 @@ let iterate_callbacks call_graph exe_env =
     Cg.get_defined_nodes call_graph in
 
   (* Make sure summaries exists. *)
-  List.iter ~f:reset_summary procs_to_analyze;
+  List.iter ~f:(fun p -> ignore (reset_summary p)) procs_to_analyze;
 
   (* Invoke procedure callbacks. *)
   List.iter
diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli
index 162313bac..1a4642770 100644
--- a/infer/src/backend/callbacks.mli
+++ b/infer/src/backend/callbacks.mli
@@ -16,7 +16,7 @@ type proc_callback_args = {
   get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
   idenv : Idenv.t;
   tenv : Tenv.t;
-  proc_name : Typ.Procname.t;
+  summary : Specs.summary;
   proc_desc : Procdesc.t;
 }
 
@@ -26,7 +26,7 @@ type proc_callback_args = {
     - Idenv to look up the definition of ids in a cfg.
     - Type environment.
     - Procedure for the callback to act on. *)
-type proc_callback_t = proc_callback_args -> unit
+type proc_callback_t = proc_callback_args -> Specs.summary
 
 type cluster_callback_t =
   Exe_env.t ->
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 7f2fd5284..f2b5265e3 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -1424,7 +1424,7 @@ let do_analysis_closures exe_env : Tasks.closure list =
       if Config.dynamic_dispatch = `Lazy
       then Some pdesc
       else None in
-    Specs.init_summary (nodes, proc_flags, calls, attributes, proc_desc_option) in
+    ignore (Specs.init_summary (nodes, proc_flags, calls, attributes, proc_desc_option)) in
 
   let callbacks =
     let get_proc_desc proc_name =
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index 3e4622008..ed96e2e0f 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -137,7 +137,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       if Config.dynamic_dispatch = `Lazy
       then Some callee_pdesc
       else None in
-    Specs.reset_summary callee_pname attributes_opt callee_pdesc_option;
+    ignore (Specs.reset_summary callee_pname attributes_opt callee_pdesc_option);
     Specs.set_status callee_pname Specs.Active;
     source in
 
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 8b8c48b4e..793cc78b7 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -745,7 +745,8 @@ let init_summary
           ProcAttributes.proc_flags = proc_flags; };
       proc_desc_option;
     } in
-  Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary
+  Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary;
+  summary
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
 let reset_summary proc_name attributes_opt proc_desc_option =
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 94724748e..79bb059e7 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -213,17 +213,17 @@ val get_status : summary -> status
 val is_active : summary -> bool
 
 (** Initialize the summary for [proc_name] given dependent procs in list [depend_list].
-    Do nothing if a summary exists already. *)
+    This also stores the new summary in the spec table. *)
 val init_summary :
   ( Procdesc.Node.id list * (* nodes *)
     ProcAttributes.proc_flags * (* procedure flags *)
     (Typ.Procname.t * Location.t) list * (* calls *)
     ProcAttributes.t * (* attributes of the procedure *)
     Procdesc.t option) (* procdesc option *)
-  -> unit
+  -> summary
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
-val reset_summary : Typ.Procname.t -> ProcAttributes.t option -> Procdesc.t option -> unit
+val reset_summary : Typ.Procname.t -> ProcAttributes.t option -> Procdesc.t option -> summary
 
 (** Load procedure summary from the given file *)
 val load_summary : DB.filename -> summary option
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 6f87422fa..131e54318 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -444,8 +444,9 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
     Dom.Summary.pp_summary F.err_formatter s;
     F.fprintf F.err_formatter "@]@."
 
-let checker : Callbacks.proc_callback_args -> unit
-  = fun ({ proc_name } as callback) ->
+let checker : Callbacks.proc_callback_args -> Specs.summary
+  = fun ({ summary } as callback) ->
+    let proc_name = Specs.get_proc_name summary in
     let make_extras _ = callback.get_proc_desc in
     let post =
       Interprocedural.compute_and_store_post
@@ -453,6 +454,9 @@ let checker : Callbacks.proc_callback_args -> unit
         ~make_extras
         callback
     in
-    match post with
-    | Some s when Config.bo_debug >= 1 -> print_summary proc_name s
-    | _ -> ()
+    begin
+      match post with
+      | Some s when Config.bo_debug >= 1 -> print_summary proc_name s
+      | _ -> ()
+    end;
+    Specs.get_summary_unsafe "bufferOverrunChecker.checker" proc_name
diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml
index fc4c0bd76..f79915728 100644
--- a/infer/src/checkers/AbstractInterpreter.ml
+++ b/infer/src/checkers/AbstractInterpreter.ml
@@ -159,7 +159,8 @@ end
 module Interprocedural (Summ : Summary.S) = struct
 
   let compute_and_store_post
-      ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } =
+      ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; tenv; } =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let analyze_ondemand_ _ pdesc =
       match compute_post (ProcData.make pdesc tenv (make_extras pdesc)) with
       | Some post ->
diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml
index d52a393db..433cefd63 100644
--- a/infer/src/checkers/BoundedCallTree.ml
+++ b/infer/src/checkers/BoundedCallTree.ml
@@ -163,20 +163,24 @@ let loaded_stacktraces =
   | None -> None
   | Some files -> Some (List.map ~f:Stacktrace.of_json_file files)
 
-let checker { Callbacks.proc_desc; tenv; get_proc_desc; } =
-  match loaded_stacktraces with
-  | None -> failwith "Missing command line option. Either \
-                      '--stacktrace stack.json' or '--stacktrace-dir ./dir' \
-                      must be used when running '-a crashcontext'. This \
-                      options expects a JSON formated stack trace or a \
-                      directory containing multiple such traces, \
-                      respectively. See \
-                      tests/codetoanalyze/java/crashcontext/*.json for \
-                      examples of the expected format."
-  | Some stacktraces -> begin
-      let extras = { get_proc_desc; stacktraces; } in
-      SpecSummary.write_summary
-        (Procdesc.get_proc_name proc_desc)
-        (Some (stacktree_of_pdesc proc_desc "proc_start"));
-      ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty)
-    end
+let checker { Callbacks.proc_desc; tenv; get_proc_desc } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  begin
+    match loaded_stacktraces with
+    | None -> failwith "Missing command line option. Either \
+                        '--stacktrace stack.json' or '--stacktrace-dir ./dir' \
+                        must be used when running '-a crashcontext'. This \
+                        options expects a JSON formated stack trace or a \
+                        directory containing multiple such traces, \
+                        respectively. See \
+                        tests/codetoanalyze/java/crashcontext/*.json for \
+                        examples of the expected format."
+    | Some stacktraces -> begin
+        let extras = { get_proc_desc; stacktraces; } in
+        SpecSummary.write_summary
+          proc_name
+          (Some (stacktree_of_pdesc proc_desc "proc_start"));
+        ignore (Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty)
+      end
+  end;
+  Specs.get_summary_unsafe "BoundedCallTree.checker" proc_name
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
index b0f7e5461..c0fbbdec5 100644
--- a/infer/src/checkers/SimpleChecker.ml
+++ b/infer/src/checkers/SimpleChecker.ml
@@ -37,7 +37,7 @@ end
 
 module type S = sig
   (** add YourChecker.checker to registerCallbacks.ml to run your checker *)
-  val checker : Callbacks.proc_callback_args -> unit
+  val checker : Callbacks.proc_callback_t
 end
 
 module Make (Spec : Spec) : S = struct
@@ -82,7 +82,8 @@ module Make (Spec : Spec) : S = struct
 
   module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
 
-  let checker { Callbacks.proc_desc; proc_name; tenv; } =
+  let checker { Callbacks.proc_desc; tenv; } : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =
       let astate_set = state.AbstractInterpreter.post in
@@ -99,5 +100,7 @@ module Make (Spec : Spec) : S = struct
           astate_set in
     let inv_map =
       Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty in
-    Analyzer.InvariantMap.iter do_reporting inv_map
+    Analyzer.InvariantMap.iter do_reporting inv_map;
+    Specs.get_summary_unsafe "checker" proc_name
+
 end
diff --git a/infer/src/checkers/SimpleChecker.mli b/infer/src/checkers/SimpleChecker.mli
index 7c1ad20e8..10ed0b4af 100644
--- a/infer/src/checkers/SimpleChecker.mli
+++ b/infer/src/checkers/SimpleChecker.mli
@@ -20,6 +20,6 @@ sig
   val compare : astate -> astate -> int
 end
 
-module type S = sig val checker : Callbacks.proc_callback_args -> unit end
+module type S = sig val checker : Callbacks.proc_callback_t end
 
 module Make : functor (Spec : Spec) -> S
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index 3c63f5d35..acb8facc3 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -243,15 +243,18 @@ let compute_post proc_data =
     ~initial:(SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty)
   |> Option.map ~f:SiofDomain.normalize
 
-let checker ({ Callbacks.proc_desc; } as callback) =
+let checker ({ Callbacks.proc_desc } as callback) : Specs.summary =
   let post =
     Interprocedural.compute_and_store_post
       ~compute_post
       ~make_extras:ProcData.make_empty_extras
       callback in
   let pname = Procdesc.get_proc_name proc_desc in
-  match Typ.Procname.get_global_name_of_initializer pname with
-  | Some gname ->
-      siof_check proc_desc gname post
-  | None ->
-      ()
+  begin
+    match Typ.Procname.get_global_name_of_initializer pname with
+    | Some gname ->
+        siof_check proc_desc gname post
+    | None ->
+        ()
+  end;
+  Specs.get_summary_unsafe "SIOF checker" pname
diff --git a/infer/src/checkers/Siof.mli b/infer/src/checkers/Siof.mli
index c99489fe0..0fecddd16 100644
--- a/infer/src/checkers/Siof.mli
+++ b/infer/src/checkers/Siof.mli
@@ -9,4 +9,4 @@
 
 open! IStd
 
-val checker: Callbacks.proc_callback_args -> unit
+val checker: Callbacks.proc_callback_t
diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index fbac36fda..a69434d5b 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/infer/src/checkers/ThreadSafety.ml
@@ -807,8 +807,10 @@ let analyze_procedure callback =
   | Some post -> post
   | None -> empty
 
-let checker callback =
-  ignore (analyze_procedure callback)
+let checker ({ Callbacks.summary } as callback_args) : Specs.summary =
+  let proc_name = Specs.get_proc_name summary in
+  ignore (analyze_procedure callback_args);
+  Specs.get_summary_unsafe "ThreadSafety.checker" proc_name
 
 (* creates a map from proc_envs to postconditions *)
 let make_results_table get_proc_desc file_env =
@@ -824,8 +826,9 @@ let make_results_table get_proc_desc file_env =
       | Some summ -> summ
       | None ->
           let callback_arg =
+            let summary = Specs.get_summary_unsafe "compute_post_for_procedure" proc_name in
             let get_procs_in_file _ = [] in
-            { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
+            { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; summary; proc_desc } in
           analyze_procedure callback_arg in
   map_post_computation_over_procs compute_post_for_procedure file_env
 
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index 0b3f459d9..22baa18fa 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -347,7 +347,8 @@ module Interprocedural = struct
   let method_is_expensive tenv pname =
     is_modeled_expensive tenv pname || is_expensive tenv pname
 
-  let check_and_report ({ Callbacks.proc_desc; proc_name; tenv; } as proc_data) =
+  let check_and_report ({ Callbacks.proc_desc; tenv; } as proc_data) : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let loc = Procdesc.get_loc proc_desc in
     let expensive = is_expensive tenv proc_name in
     (* TODO: generalize so we can check subtyping on arbitrary annotations *)
@@ -397,14 +398,18 @@ module Interprocedural = struct
           (src_snk_pairs ()) in
       Domain.NonBottom
         (init_map, Domain.TrackingVar.empty) in
-    match compute_and_store_post
-            ~compute_post:(Analyzer.compute_post ~initial)
-            ~make_extras:ProcData.make_empty_extras
-            proc_data with
-    | Some Domain.NonBottom (call_map, _) ->
-        List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ())
-    | Some Domain.Bottom | None ->
-        ()
+    begin
+      match compute_and_store_post
+              ~compute_post:(Analyzer.compute_post ~initial)
+              ~make_extras:ProcData.make_empty_extras
+              proc_data with
+      | Some Domain.NonBottom (call_map, _) ->
+          List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ())
+      | Some Domain.Bottom | None ->
+          ()
+    end;
+    Specs.get_summary_unsafe "AnnotationReachability.checker" proc_name
+
 end
 
 let checker = Interprocedural.check_and_report
diff --git a/infer/src/checkers/checkDeadCode.ml b/infer/src/checkers/checkDeadCode.ml
index 28b58befc..2254d6e50 100644
--- a/infer/src/checkers/checkDeadCode.ml
+++ b/infer/src/checkers/checkDeadCode.ml
@@ -91,7 +91,8 @@ let check_final_state tenv proc_name proc_desc final_s =
     end
 
 (** Simple check for dead code. *)
-let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
+let callback_check_dead_code { Callbacks.proc_desc; tenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
 
   let module DFDead = MakeDF(struct
       type t = State.t
@@ -113,4 +114,5 @@ let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
       | DFDead.Dead_state -> ()
     end in
 
-  do_check ()
+  do_check ();
+  Specs.get_summary_unsafe "callback_check_dead_code" proc_name
diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml
index e5d071a0b..7bf127d55 100644
--- a/infer/src/checkers/checkTraceCallSequence.ml
+++ b/infer/src/checkers/checkTraceCallSequence.ml
@@ -317,7 +317,8 @@ let check_final_state tenv proc_name proc_desc exit_node final_s =
 (** Check that the trace calls are balanced.
     This is done by using the most general control flow including exceptions.
     The begin() and end() function are assumed not to throw exceptions. *)
-let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv; tenv } : unit =
+let callback_check_trace_call_sequence { Callbacks.proc_desc; idenv; tenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
 
   let module DFTrace = MakeDF(struct
       type t = State.t
@@ -341,4 +342,5 @@ let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv;
       | DFTrace.Dead_state -> ()
     end in
 
-  if not (APIs.is_begin_or_end proc_name) then do_check ()
+  if not (APIs.is_begin_or_end proc_name) then do_check ();
+  Specs.get_summary_unsafe "callback_check_trace_call_sequence" proc_name
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index c3672d4ac..73cfd1206 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -168,10 +168,12 @@ let report_calls_and_accesses tenv callback proc_desc instr =
       | None -> ()
 
 (** Report all field accesses and method calls of a procedure. *)
-let callback_check_access { Callbacks.tenv; proc_desc } =
+let callback_check_access { Callbacks.tenv; proc_desc; } =
   Procdesc.iter_instrs
     (fun _ instr  -> report_calls_and_accesses tenv Localise.proc_callback proc_desc instr)
-    proc_desc
+    proc_desc;
+  Specs.get_summary_unsafe "callback_check_access" (Procdesc.get_proc_name proc_desc)
+
 
 (** Report all field accesses and method calls of a class. *)
 let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
@@ -189,7 +191,8 @@ let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
 
 (** Looks for writeToParcel methods and checks whether read is in reverse *)
 let callback_check_write_to_parcel_java
-    pname_java ({ Callbacks.tenv; proc_desc; idenv; get_proc_desc } as args) =
+    pname_java { Callbacks.tenv; proc_desc; idenv; get_proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = ref false in
 
   let is_write_to_parcel this_expr this_type =
@@ -265,17 +268,17 @@ let callback_check_write_to_parcel_java
       | rc:: rcs, wc:: wcs ->
           if not (is_inverse rc wc) then
             L.stdout "Serialization missmatch in %a for %a and %a@."
-              Typ.Procname.pp args.Callbacks.proc_name
+              Typ.Procname.pp proc_name
               Typ.Procname.pp rc
               Typ.Procname.pp wc
           else
             check_match (rcs, wcs)
       | rc:: _, [] ->
           L.stdout "Missing write in %a: for %a@."
-            Typ.Procname.pp args.Callbacks.proc_name Typ.Procname.pp rc
+            Typ.Procname.pp proc_name Typ.Procname.pp rc
       | _, wc:: _ ->
           L.stdout "Missing read in %a: for %a@."
-            Typ.Procname.pp args.Callbacks.proc_name Typ.Procname.pp wc
+            Typ.Procname.pp proc_name Typ.Procname.pp wc
       | _ ->
           () in
 
@@ -287,7 +290,7 @@ let callback_check_write_to_parcel_java
         if is_write_to_parcel this_exp this_type then begin
           if !verbose then
             L.stdout "Serialization check for %a@."
-              Typ.Procname.pp args.Callbacks.proc_name;
+              Typ.Procname.pp proc_name;
           try
             match parcel_constructors tenv this_type with
             | x :: _ ->
@@ -296,7 +299,7 @@ let callback_check_write_to_parcel_java
                  | None -> raise Not_found)
             | _ ->
                 L.stdout "No parcel constructor found for %a@."
-                  Typ.Procname.pp args.Callbacks.proc_name
+                  Typ.Procname.pp proc_name
           with Not_found ->
             if !verbose then L.stdout "Methods not available@."
         end
@@ -304,15 +307,18 @@ let callback_check_write_to_parcel_java
   Procdesc.iter_instrs do_instr proc_desc
 
 (** Looks for writeToParcel methods and checks whether read is in reverse *)
-let callback_check_write_to_parcel ({ Callbacks.proc_name } as args) =
-  match proc_name with
-  | Typ.Procname.Java pname_java ->
-      callback_check_write_to_parcel_java pname_java args
-  | _ ->
-      ()
+let callback_check_write_to_parcel ({ Callbacks.summary } as args) =
+  begin
+    match Specs.get_proc_name summary with
+    | Typ.Procname.Java pname_java ->
+        callback_check_write_to_parcel_java pname_java args
+    | _ -> ()
+  end;
+  summary
 
 (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *)
-let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
+let callback_monitor_nullcheck { Callbacks.proc_desc; idenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = ref false in
 
   let class_formal_names = lazy (
@@ -389,23 +395,28 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
                ())
     | _ -> () in
   Procdesc.iter_instrs do_instr proc_desc;
-  summary_checks_of_formals ()
+  summary_checks_of_formals ();
+  Specs.get_summary_unsafe "callback_monitor_nullcheck" proc_name
 
 (** Test persistent state. *)
-let callback_test_state { Callbacks.proc_name } =
-  ST.pname_add proc_name "somekey" "somevalue"
+let callback_test_state { Callbacks.summary } =
+  let proc_name = Specs.get_proc_name summary in
+  ST.pname_add proc_name "somekey" "somevalue";
+  Specs.get_summary_unsafe "callback_test_state" proc_name
 
 (** Check the uses of VisibleForTesting *)
-let callback_checkVisibleForTesting { Callbacks.proc_desc } =
+let callback_checkVisibleForTesting { Callbacks.proc_desc; summary } =
   if Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting then
     begin
       let loc = Procdesc.get_loc proc_desc in
       let linereader = Printer.LineReader.create () in
       L.stdout "%a@." (PP.pp_loc_range linereader 10 10) loc
-    end
+    end;
+  summary
 
 (** Check for readValue and readValueAs json deserialization *)
-let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; proc_name } =
+let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = true in
 
   let ret_const_key = "return_const" in
@@ -498,10 +509,11 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
     ST.pname_add proc_name ret_const_key ret_const in
 
   store_return ();
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_find_deserialization" proc_name
 
 (** Check field accesses. *)
-let callback_check_field_access { Callbacks.proc_desc } =
+let callback_check_field_access { Callbacks.proc_desc; summary } =
   let rec do_exp is_read = function
     | Exp.Var _ -> ()
     | Exp.UnOp (_, e, _) ->
@@ -541,10 +553,12 @@ let callback_check_field_access { Callbacks.proc_desc } =
     | Sil.Remove_temps _
     | Sil.Declare_locals _ ->
         () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  summary
 
 (** Print c method calls. *)
-let callback_print_c_method_calls { Callbacks.tenv; proc_desc; proc_name } =
+let callback_print_c_method_calls { Callbacks.tenv; proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let do_instr node = function
     | Sil.Call (_, Exp.Const (Const.Cfun pn), (e, _):: _, loc, _)
       when Typ.Procname.is_c_method pn ->
@@ -569,10 +583,12 @@ let callback_print_c_method_calls { Callbacks.tenv; proc_desc; proc_name } =
           loc
           description
     | _ -> () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_print_c_method_calls" proc_name
 
 (** Print access to globals. *)
-let callback_print_access_to_globals { Callbacks.tenv; proc_desc; proc_name } =
+let callback_print_access_to_globals { Callbacks.tenv; proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let do_pvar is_read pvar loc =
     let description =
       Printf.sprintf "%s of global %s"
@@ -597,4 +613,5 @@ let callback_print_access_to_globals { Callbacks.tenv; proc_desc; proc_name } =
     | Sil.Store (e, _, _, loc) when get_global_var e <> None ->
         Option.iter ~f:(fun pvar -> do_pvar false pvar loc) (get_global_var e)
     | _ -> () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_print_access_to_globals" proc_name
diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml
index 87a8a3b7e..c37f9f493 100644
--- a/infer/src/checkers/dataflow.ml
+++ b/infer/src/checkers/dataflow.ml
@@ -171,7 +171,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
 end (* MakeDF *)
 
 (** Example dataflow callback: compute the the distance from a node to the start node. *)
-let callback_test_dataflow { Callbacks.proc_desc; tenv } =
+let callback_test_dataflow { Callbacks.proc_desc; tenv; summary } =
   let verbose = false in
   let module DFCount = MakeDF(struct
       type t = int
@@ -187,4 +187,5 @@ let callback_test_dataflow { Callbacks.proc_desc; tenv } =
     match transitions node with
     | DFCount.Transition _ -> ()
     | DFCount.Dead_state -> () in
-  List.iter ~f:do_node (Procdesc.get_nodes proc_desc)
+  List.iter ~f:do_node (Procdesc.get_nodes proc_desc);
+  summary
diff --git a/infer/src/checkers/fragmentRetainsViewChecker.ml b/infer/src/checkers/fragmentRetainsViewChecker.ml
index 48218e95b..fbc4c1223 100644
--- a/infer/src/checkers/fragmentRetainsViewChecker.ml
+++ b/infer/src/checkers/fragmentRetainsViewChecker.ml
@@ -51,9 +51,13 @@ let callback_fragment_retains_view_java
       | _ -> ()
     end
 
-let callback_fragment_retains_view ({ Callbacks.proc_name } as args) =
-  match proc_name with
-  | Typ.Procname.Java pname_java ->
-      callback_fragment_retains_view_java pname_java args
-  | _ ->
-      ()
+let callback_fragment_retains_view ({ Callbacks.summary } as args) : Specs.summary =
+  let proc_name = Specs.get_proc_name summary in
+  begin
+    match proc_name  with
+    | Typ.Procname.Java pname_java ->
+        callback_fragment_retains_view_java pname_java args
+    | _ ->
+        ()
+  end;
+  Specs.get_summary_unsafe "callback_fragment_retains_view" proc_name
diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml
index e35e5bfea..d6d0f7888 100644
--- a/infer/src/checkers/printfArgs.ml
+++ b/infer/src/checkers/printfArgs.ml
@@ -206,8 +206,10 @@ let check_printf_args_ok tenv
       | None -> ())
   | _ -> ()
 
-let callback_printf_args { Callbacks.tenv; proc_desc; proc_name } : unit =
-  Procdesc.iter_instrs (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc) proc_desc
+let callback_printf_args { Callbacks.tenv; proc_desc } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  Procdesc.iter_instrs (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc) proc_desc;
+  Specs.get_summary_unsafe "Callbacks.proc_callback_t" proc_name
 
 (*
 let printf_signature_to_string
diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml
index e96c58492..6d67953d4 100644
--- a/infer/src/checkers/sqlChecker.ml
+++ b/infer/src/checkers/sqlChecker.ml
@@ -13,7 +13,8 @@ module L = Logging
 
 
 (** Find SQL statements in string concatenations *)
-let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
+let callback_sql { Callbacks.proc_desc; tenv } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = false in
 
   (* Case insensitive SQL statement patterns *)
@@ -63,8 +64,11 @@ let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
         end
     | _ -> () in
 
-  try
-    let const_map = ConstantPropagation.build_const_map tenv proc_desc in
-    if verbose then L.stdout "Analyzing %a...\n@." Typ.Procname.pp proc_name;
-    Procdesc.iter_instrs (do_instr const_map) proc_desc
-  with _ -> ()
+  begin
+    try
+      let const_map = ConstantPropagation.build_const_map tenv proc_desc in
+      if verbose then L.stdout "Analyzing %a...\n@." Typ.Procname.pp proc_name;
+      Procdesc.iter_instrs (do_instr const_map) proc_desc
+    with _ -> ()
+  end;
+  Specs.get_summary_unsafe "SqlChecker.callback_sql" proc_name
diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml
index 904836545..4b3887357 100644
--- a/infer/src/eradicate/eradicate.ml
+++ b/infer/src/eradicate/eradicate.ml
@@ -27,7 +27,7 @@ type parameters = TypeState.parameters
 (** Type for a module that provides a main callback function *)
 module type CallBackT =
 sig
-  val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
+  val callback : TypeCheck.checks -> Callbacks.proc_callback_t
 end (* CallBackT *)
 
 (** Extension to the type checker. *)
@@ -153,13 +153,14 @@ struct
       calls_this checks
       {
         Callbacks.proc_desc = curr_pdesc;
-        proc_name = curr_pname;
+        summary;
         get_proc_desc;
         idenv;
         tenv;
         get_procs_in_file;
       }
       annotated_signature linereader proc_loc : unit =
+    let curr_pname = Specs.get_proc_name summary in
 
     let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
     let find_canonical_duplicate node =
@@ -340,7 +341,8 @@ struct
     update_summary curr_pname curr_pdesc final_typestate_opt
 
   (** Entry point for the eradicate-based checker infrastructure. *)
-  let callback checks ({ Callbacks.proc_desc; proc_name } as callback_args) =
+  let callback checks ({ Callbacks.proc_desc } as callback_args) : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let calls_this = ref false in
 
     let filter_special_cases () =
@@ -353,16 +355,19 @@ struct
             Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in
           Some annotated_signature
         end in
-    match filter_special_cases () with
-    | None -> ()
-    | Some annotated_signature ->
-        let loc = Procdesc.get_loc proc_desc in
-        let linereader = Printer.LineReader.create () in
-        if Config.eradicate_verbose then
-          L.stdout "%a@." (AnnotatedSignature.pp proc_name) annotated_signature;
+    begin
+      match filter_special_cases () with
+      | None -> ()
+      | Some annotated_signature ->
+          let loc = Procdesc.get_loc proc_desc in
+          let linereader = Printer.LineReader.create () in
+          if Config.eradicate_verbose then
+            L.stdout "%a@." (AnnotatedSignature.pp proc_name) annotated_signature;
 
-        callback2
-          calls_this checks callback_args annotated_signature linereader loc
+          callback2
+            calls_this checks callback_args annotated_signature linereader loc
+    end;
+    Specs.get_summary_unsafe "callback" proc_name
 
 end (* MkCallback *)
 
@@ -399,7 +404,7 @@ module Main =
 
 (** Eradicate checker for Java @Nullable annotations. *)
 let callback_eradicate
-    ({ Callbacks.get_proc_desc; proc_name } as callback_args) =
+    ({ Callbacks.get_proc_desc; summary } as callback_args) =
   let checks =
     {
       TypeCheck.eradicate = true;
@@ -409,24 +414,28 @@ let callback_eradicate
   let callbacks =
     let analyze_ondemand _ pdesc =
       let idenv_pname = Idenv.create pdesc in
+      let proc_name = Procdesc.get_proc_name pdesc in
+      let summary = Specs.get_summary_unsafe "Eradicate.analyze_ondemand" proc_name in
       Main.callback checks
         { callback_args with
           Callbacks.idenv = idenv_pname;
-          proc_name = (Procdesc.get_proc_name pdesc);
-          proc_desc = pdesc; };
-      Specs.get_summary_unsafe "callback_eradicate" (Procdesc.get_proc_name pdesc) in
+          summary;
+          proc_desc = pdesc; } in
     {
       Ondemand.analyze_ondemand;
       get_proc_desc;
     } in
 
-  if Ondemand.procedure_should_be_analyzed proc_name
+  if Ondemand.procedure_should_be_analyzed (Specs.get_proc_name summary)
   then
     begin
       Ondemand.set_callbacks callbacks;
-      Main.callback checks callback_args;
-      Ondemand.unset_callbacks ()
+      let final_summary = Main.callback checks callback_args in
+      Ondemand.unset_callbacks ();
+      final_summary
     end
+  else
+    summary
 
 (** Call the given check_return_type at the end of every procedure. *)
 let callback_check_return_type check_return_type callback_args =
diff --git a/infer/src/eradicate/eradicate.mli b/infer/src/eradicate/eradicate.mli
index ba3497dae..6caef9937 100644
--- a/infer/src/eradicate/eradicate.mli
+++ b/infer/src/eradicate/eradicate.mli
@@ -23,7 +23,7 @@ type parameters = (Exp.t * Typ.t) list
 (** Type for a module that provides a main callback function *)
 module type CallBackT =
 sig
-  val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
+  val callback : TypeCheck.checks -> Callbacks.proc_callback_t
 end (* CallBackT *)
 
 
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 091f0ce31..d1faa20b0 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -495,7 +495,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
   module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
 
-  let checker ({ Callbacks.tenv } as callback) =
+  let checker ({ Callbacks.tenv; summary } as callback) : Specs.summary =
+    let proc_name = Specs.get_proc_name summary in
 
     (* bind parameters to a trace with a tainted source (if applicable) *)
     let make_initial pdesc =
@@ -530,5 +531,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           then failwith "Couldn't compute post"
           else None in
     let make_extras = FormalMap.make in
-    ignore(Interprocedural.compute_and_store_post ~compute_post ~make_extras callback)
+    ignore (Interprocedural.compute_and_store_post ~compute_post ~make_extras callback);
+    Specs.get_summary_unsafe "taint analysis" proc_name
 end