diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 9eacd2afc..636d481b7 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -188,7 +188,7 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
 
   (* Note on narrowing operations: we defines the narrowing operations simply to take a smaller one.
      So, as of now, the termination of narrowing is not guaranteed in general. *)
-  let exec_node ~pp_instr ({ProcData.pdesc} as proc_data) node ~is_loop_head ~is_narrowing
+  let exec_node ~pp_instr ({ProcData.summary} as proc_data) node ~is_loop_head ~is_narrowing
       astate_pre inv_map =
     let node_id = Node.id node in
     let update_inv_map pre ~visit_count =
@@ -218,10 +218,12 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
         else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then (
           L.(debug Analysis Verbose)
             "Terminate narrowing because old and new states are not comparable at %a:%a@."
-            Typ.Procname.pp (Procdesc.get_proc_name pdesc) Node.pp_id node_id ;
+            Typ.Procname.pp (Summary.get_proc_name summary) Node.pp_id node_id ;
           (inv_map, ReachedFixPoint) )
         else
-          let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in
+          let visit_count' =
+            VisitCount.succ ~pdesc:(Summary.get_proc_desc summary) old_state.State.visit_count
+          in
           update_inv_map new_pre ~visit_count:visit_count'
       else
         (* first time visiting this node *)
@@ -268,15 +270,16 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
 
 
   (** compute and return an invariant map for [pdesc] *)
-  let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~do_narrowing ~initial =
-    exec_cfg_internal ~pp_instr:pp_sil_instr (CFG.from_pdesc pdesc) proc_data ~do_narrowing
-      ~initial
+  let make_exec_pdesc ~exec_cfg_internal ({ProcData.summary} as proc_data) ~do_narrowing ~initial =
+    exec_cfg_internal ~pp_instr:pp_sil_instr
+      (CFG.from_pdesc (Summary.get_proc_desc summary))
+      proc_data ~do_narrowing ~initial
 
 
   (** compute and return the postcondition of [pdesc] *)
   let make_compute_post ~exec_cfg_internal ?(pp_instr = pp_sil_instr)
-      ({ProcData.pdesc} as proc_data) ~do_narrowing ~initial =
-    let cfg = CFG.from_pdesc pdesc in
+      ({ProcData.summary} as proc_data) ~do_narrowing ~initial =
+    let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in
     let inv_map = exec_cfg_internal ~pp_instr cfg proc_data ~do_narrowing ~initial in
     extract_post (Node.id (CFG.exit_node cfg)) inv_map
 end
@@ -287,7 +290,7 @@ module MakeWithScheduler
 struct
   include AbstractInterpreterCommon (TransferFunctions)
 
-  let rec exec_worklist ~pp_instr cfg ({ProcData.pdesc} as proc_data) work_queue inv_map =
+  let rec exec_worklist ~pp_instr cfg ({ProcData.summary} as proc_data) work_queue inv_map =
     match Scheduler.pop work_queue with
     | Some (_, [], work_queue') ->
         exec_worklist ~pp_instr cfg proc_data work_queue' inv_map
@@ -295,7 +298,7 @@ struct
         let inv_map_post, work_queue_post =
           match compute_pre cfg node inv_map with
           | Some astate_pre -> (
-              let is_loop_head = CFG.is_loop_head pdesc node in
+              let is_loop_head = CFG.is_loop_head (Summary.get_proc_desc summary) node in
               match
                 exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing:false astate_pre
                   inv_map
diff --git a/infer/src/absint/ProcData.ml b/infer/src/absint/ProcData.ml
index c77ab2a6a..06a675afe 100644
--- a/infer/src/absint/ProcData.ml
+++ b/infer/src/absint/ProcData.ml
@@ -7,12 +7,12 @@
 
 open! IStd
 
-type 'a t = {pdesc: Procdesc.t; tenv: Tenv.t; extras: 'a}
+type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a}
 
 type no_extras = unit
 
 let empty_extras = ()
 
-let make pdesc tenv extras = {pdesc; tenv; extras}
+let make summary tenv extras = {summary; tenv; extras}
 
-let make_default pdesc tenv = make pdesc tenv empty_extras
+let make_default summary tenv = make summary tenv empty_extras
diff --git a/infer/src/absint/ProcData.mli b/infer/src/absint/ProcData.mli
index 4452cb829..743f93f22 100644
--- a/infer/src/absint/ProcData.mli
+++ b/infer/src/absint/ProcData.mli
@@ -7,12 +7,12 @@
 
 open! IStd
 
-type 'a t = {pdesc: Procdesc.t; tenv: Tenv.t; extras: 'a}
+type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a}
 
 type no_extras
 
 val empty_extras : no_extras
 
-val make : Procdesc.t -> Tenv.t -> 'a -> 'a t
+val make : Summary.t -> Tenv.t -> 'a -> 'a t
 
-val make_default : Procdesc.t -> Tenv.t -> no_extras t
+val make_default : Summary.t -> Tenv.t -> no_extras t
diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml
index 48c28fa8b..262361018 100644
--- a/infer/src/backend/preanal.ml
+++ b/infer/src/backend/preanal.ml
@@ -123,20 +123,20 @@ end
 
 module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions)
 
-let add_nullify_instrs pdesc tenv liveness_inv_map =
+let add_nullify_instrs summary tenv liveness_inv_map =
   let address_taken_vars =
-    if Typ.Procname.is_java (Procdesc.get_proc_name pdesc) then AddressTaken.Domain.empty
+    if Typ.Procname.is_java (Summary.get_proc_name summary) then AddressTaken.Domain.empty
       (* can't take the address of a variable in Java *)
     else
       let initial = AddressTaken.Domain.empty in
-      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) ~initial with
+      match AddressTaken.Analyzer.compute_post (ProcData.make_default summary tenv) ~initial with
       | Some post ->
           post
       | None ->
           AddressTaken.Domain.empty
   in
-  let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in
-  let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in
+  let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc (Summary.get_proc_desc summary) in
+  let nullify_proc_data = ProcData.make summary tenv liveness_inv_map in
   let initial = (VarDomain.empty, VarDomain.empty) in
   let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in
   (* only nullify pvars that are local; don't nullify those that can escape *)
@@ -189,28 +189,30 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
 
 (** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it
     easy for analyses to do abstract garbage collection *)
-let do_liveness pdesc tenv =
-  let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
+let do_liveness summary tenv =
+  let liveness_proc_cfg = BackwardCfg.from_pdesc (Summary.get_proc_desc summary) in
   let initial = Liveness.Domain.empty in
   let liveness_inv_map =
-    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) ~initial
+    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default summary tenv) ~initial
   in
-  add_nullify_instrs pdesc tenv liveness_inv_map
+  add_nullify_instrs summary tenv liveness_inv_map
 
 
 (** add Abstract instructions into the IR to give hints about when abstraction should be
     performed *)
 let do_abstraction pdesc = add_abstraction_instructions pdesc
 
-let do_funptr_sub pdesc tenv =
-  let updated = FunctionPointers.substitute_function_pointers pdesc tenv in
+let do_funptr_sub summary tenv =
+  let updated = FunctionPointers.substitute_function_pointers summary tenv in
+  let pdesc = Summary.get_proc_desc summary in
   if updated then Attributes.store ~proc_desc:(Some pdesc) (Procdesc.get_attributes pdesc)
 
 
 let do_preanalysis pdesc tenv =
+  let summary = Summary.reset pdesc in
   if
     Config.function_pointer_specialization
     && not (Typ.Procname.is_java (Procdesc.get_proc_name pdesc))
-  then do_funptr_sub pdesc tenv ;
-  do_liveness pdesc tenv ;
+  then do_funptr_sub summary tenv ;
+  do_liveness summary tenv ;
   do_abstraction pdesc
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index d979d5a20..8ee7732f4 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
@@ -31,9 +31,9 @@ type extras = {get_proc_summary_and_formals: get_proc_summary_and_formals; oenv:
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 module Init = struct
-  let initial_state {ProcData.pdesc; tenv; extras= {oenv}} start_node =
+  let initial_state {ProcData.summary; tenv; extras= {oenv}} start_node =
     let try_decl_local =
-      let pname = Procdesc.get_proc_name pdesc in
+      let pname = Summary.get_proc_name summary in
       let model_env =
         let node_hash = CFG.Node.hash start_node in
         let location = CFG.Node.loc start_node in
@@ -45,7 +45,10 @@ module Init = struct
         BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ)
     in
     let mem = Dom.Mem.init oenv in
-    let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
+    let mem, _ =
+      List.fold ~f:try_decl_local ~init:(mem, 1)
+        (Procdesc.get_locals (Summary.get_proc_desc summary))
+    in
     mem
 end
 
@@ -159,8 +162,8 @@ module TransferFunctions = struct
 
 
   let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-   fun mem {pdesc; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node
-       instr ->
+   fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}}
+       node instr ->
     match instr with
     | Load (id, _, _, _) when Ident.is_none id ->
         mem
@@ -185,7 +188,7 @@ module TransferFunctions = struct
     | Store (exp1, _, Const (Const.Cstr s), location) ->
         let locs = Sem.eval_locs exp1 mem in
         let model_env =
-          let pname = Procdesc.get_proc_name pdesc in
+          let pname = Summary.get_proc_name summary in
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
         in
@@ -216,10 +219,10 @@ module TransferFunctions = struct
           if not v.represents_multiple_values then
             match PowLoc.is_singleton_or_more locs with
             | IContainer.Singleton loc_v -> (
-                let pname = Procdesc.get_proc_name pdesc in
+                let pname = Summary.get_proc_name summary in
                 match Typ.Procname.get_method pname with
                 | "__inferbo_empty" when Loc.is_return loc_v -> (
-                  match Procdesc.get_pvar_formals pdesc with
+                  match Procdesc.get_pvar_formals (Summary.get_proc_desc summary) with
                   | [(formal, _)] ->
                       let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in
                       Dom.Mem.store_empty_alias formal_v loc_v mem
@@ -268,7 +271,7 @@ module TransferFunctions = struct
         Dom.Mem.add_unknown id ~location mem
     | Metadata (VariableLifetimeBegins (pvar, typ, location)) when Pvar.is_global pvar ->
         let model_env =
-          let pname = Procdesc.get_proc_name pdesc in
+          let pname = Summary.get_proc_name summary in
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
         in
@@ -309,12 +312,13 @@ let get_local_decls : Procdesc.t -> local_decls =
 
 
 let compute_invariant_map :
-    Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map =
- fun pdesc tenv integer_type_widths get_proc_summary_and_formals ->
+    Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map =
+ fun summary tenv integer_type_widths get_proc_summary_and_formals ->
+  let pdesc = Summary.get_proc_desc summary in
   let cfg = CFG.from_pdesc pdesc in
   let pdata =
     let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in
-    ProcData.make pdesc tenv {get_proc_summary_and_formals; oenv}
+    ProcData.make summary tenv {get_proc_summary_and_formals; oenv}
   in
   let initial = Init.initial_state pdata (CFG.start_node cfg) in
   Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata
@@ -330,8 +334,8 @@ let cached_compute_invariant_map =
     let hash (pname, _) = Hashtbl.hash pname
   end) in
   let inv_map_cache = WeakInvMapHashTbl.create 100 in
-  fun pdesc tenv integer_type_widths ->
-    let pname = Procdesc.get_proc_name pdesc in
+  fun summary tenv integer_type_widths ->
+    let pname = Summary.get_proc_name summary in
     match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with
     | Some (_, Some inv_map) ->
         inv_map
@@ -340,14 +344,14 @@ let cached_compute_invariant_map =
         assert false
     | None ->
         let get_proc_summary_and_formals callee_pname =
-          Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
+          Ondemand.analyze_proc_name ~caller_pdesc:(Summary.get_proc_desc summary) callee_pname
           |> Option.bind ~f:(fun summary ->
                  Payload.of_summary summary
                  |> Option.map ~f:(fun payload ->
                         (payload, Summary.get_proc_desc summary |> Procdesc.get_pvar_formals) ) )
         in
         let inv_map =
-          compute_invariant_map pdesc tenv integer_type_widths get_proc_summary_and_formals
+          compute_invariant_map summary tenv integer_type_widths get_proc_summary_and_formals
         in
         WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ;
         inv_map
@@ -370,7 +374,7 @@ let compute_summary :
 let do_analysis : Callbacks.proc_callback_args -> Summary.t =
  fun {tenv; integer_type_widths; summary} ->
   let proc_desc = Summary.get_proc_desc summary in
-  let inv_map = cached_compute_invariant_map proc_desc tenv integer_type_widths in
+  let inv_map = cached_compute_invariant_map summary tenv integer_type_widths in
   let locals = get_local_decls proc_desc in
   let formals = Procdesc.get_pvar_formals proc_desc in
   let cfg = CFG.from_pdesc proc_desc in
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli
index 455c119de..7ccf5b0e4 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli
@@ -14,7 +14,7 @@ type invariant_map
 
 type local_decls = AbsLoc.PowLoc.t
 
-val cached_compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map
+val cached_compute_invariant_map : Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map
 
 val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
 
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index b7154b294..7617e952d 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -425,7 +425,7 @@ let checker : Callbacks.proc_callback_args -> Summary.t =
  fun {tenv; integer_type_widths; summary} ->
   let proc_desc = Summary.get_proc_desc summary in
   let inv_map =
-    BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths
+    BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
   in
   let underlying_exit_node = Procdesc.get_exit_node proc_desc in
   let pp_name f = F.pp_print_string f "bufferoverrun check" in
diff --git a/infer/src/checkers/Litho.ml b/infer/src/checkers/Litho.ml
index 8655b56db..69f1e8047 100644
--- a/infer/src/checkers/Litho.ml
+++ b/infer/src/checkers/Litho.ml
@@ -207,7 +207,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let exec_instr astate (proc_data : extras ProcData.t) _ (instr : HilInstr.t) : Domain.t =
-    let caller_pname = Procdesc.get_proc_name proc_data.pdesc in
+    let caller_pname = Summary.get_proc_name proc_data.summary in
     match instr with
     | Call
         ( return_base
@@ -215,7 +215,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         , (HilExp.AccessExpression receiver_ae :: _ as actuals)
         , _
         , _ ) ->
-        let summary = Payload.read proc_data.pdesc callee_procname in
+        let domain_summary =
+          Payload.read (Summary.get_proc_desc proc_data.summary) callee_procname
+        in
         let receiver =
           Domain.LocalAccessPath.make
             (HilExp.AccessExpression.to_access_path receiver_ae)
@@ -224,7 +226,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         if
           ( LithoFramework.is_component_builder callee_procname proc_data.tenv
           (* track Builder's in order to check required prop's *)
-          || GraphQLGetters.is_function callee_procname summary
+          || GraphQLGetters.is_function callee_procname domain_summary
           || (* track GraphQL getters in order to report graphql field accesses *)
              Domain.mem receiver astate
              (* track anything called on a receiver we're already tracking *) )
@@ -243,9 +245,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           Domain.add return_access_path return_calls astate
         else
           (* treat it like a normal call *)
-          apply_callee_summary summary caller_pname return_base actuals astate
+          apply_callee_summary domain_summary caller_pname return_base actuals astate
     | Call (ret_id_typ, Direct callee_procname, actuals, _, _) ->
-        let summary = Payload.read proc_data.pdesc callee_procname in
+        let summary = Payload.read (Summary.get_proc_desc proc_data.summary) callee_procname in
         apply_callee_summary summary caller_pname ret_id_typ actuals astate
     | Assign (lhs_ae, HilExp.AccessExpression rhs_ae, _) -> (
         (* creating an alias for the rhs binding; assume all reads will now occur through the
@@ -272,7 +274,7 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.E
 
 let checker {Callbacks.summary; tenv} =
   let proc_desc = Summary.get_proc_desc summary in
-  let proc_data = ProcData.make_default proc_desc tenv in
+  let proc_data = ProcData.make_default summary tenv in
   match Analyzer.compute_post proc_data ~initial:Domain.empty with
   | Some post ->
       if RequiredProps.should_report proc_desc tenv then RequiredProps.report post tenv summary ;
diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml
index 95c76d535..b2b9fbb6f 100644
--- a/infer/src/checkers/NullabilityPreanalysis.ml
+++ b/infer/src/checkers/NullabilityPreanalysis.ml
@@ -97,7 +97,7 @@ let analysis cfg tenv =
     if Procdesc.is_defined pdesc && Typ.Procname.is_constructor proc_name then
       match
         FieldsAssignedInConstructorsChecker.compute_post
-          (ProcData.make pdesc tenv (Ident.Hash.create 10))
+          (ProcData.make (Summary.reset pdesc) tenv (Ident.Hash.create 10))
           ~initial
       with
       | Some new_domain ->
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
index ce43b5218..739fb4cee 100644
--- a/infer/src/checkers/SimpleChecker.ml
+++ b/infer/src/checkers/SimpleChecker.ml
@@ -67,7 +67,7 @@ module Make (Spec : Spec) : S = struct
 
     let exec_instr astate_set proc_data node instr =
       let node_kind = CFG.Node.kind node in
-      let pname = Procdesc.get_proc_name proc_data.ProcData.pdesc in
+      let pname = Summary.get_proc_name proc_data.ProcData.summary in
       Domain.fold
         (fun astate acc ->
           Domain.add (Spec.exec_instr astate instr node_kind pname proc_data.ProcData.tenv) acc )
@@ -96,9 +96,7 @@ module Make (Spec : Spec) : S = struct
           (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name)
           astate_set
     in
-    let inv_map =
-      Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty
-    in
+    let inv_map = Analyzer.exec_pdesc (ProcData.make_default summary tenv) ~initial:Domain.empty in
     Analyzer.InvariantMap.iter do_reporting inv_map ;
     summary
 end
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index 5278c7d4d..5a39ccb87 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -134,7 +134,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let at_least_nonbottom = Domain.join (NonBottom SiofTrace.bottom, Domain.VarNames.empty)
 
-  let exec_instr astate {ProcData.pdesc} _ (instr : Sil.instr) =
+  let exec_instr astate {ProcData.summary} _ (instr : Sil.instr) =
+    let pdesc = Summary.get_proc_desc summary in
     match instr with
     | Store (Lvar global, Typ.{desc= Tptr _}, Lvar _, loc)
       when (Option.equal Typ.Procname.equal)
@@ -282,7 +283,7 @@ let checker {Callbacks.tenv; summary; get_procs_in_file} : Summary.t =
     in
     includes_iostream (Procdesc.get_attributes proc_desc).ProcAttributes.translation_unit
   in
-  let proc_data = ProcData.make_default proc_desc tenv in
+  let proc_data = ProcData.make_default summary tenv in
   let initial =
     ( Bottom
     , if standard_streams_initialized_in_tu then SiofDomain.VarNames.of_list standard_streams
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index 42637455b..4720b9f55 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -588,10 +588,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           callee_call_map astate
 
 
-  let exec_instr astate {ProcData.pdesc; tenv; ProcData.extras} _ = function
+  let exec_instr astate {ProcData.summary; tenv; ProcData.extras} _ = function
     | Sil.Call ((id, _), Const (Cfun callee_pname), _, _, _) when is_unlikely callee_pname ->
         Domain.add_tracking_var (Var.of_id id) astate
     | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) ->
+        let pdesc = Summary.get_proc_desc summary in
         let caller_pname = Procdesc.get_proc_name pdesc in
         let call_site = CallSite.make callee_pname call_loc in
         check_call tenv callee_pname caller_pname call_site astate extras
@@ -617,7 +618,7 @@ let checker ({Callbacks.tenv; summary} as callback) : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in
   let specs = get_annot_specs (Procdesc.get_proc_name proc_desc) in
-  let proc_data = ProcData.make proc_desc tenv specs in
+  let proc_data = ProcData.make summary tenv specs in
   match Analyzer.compute_post proc_data ~initial with
   | Some (annot_map, _) ->
       List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report callback annot_map) ;
diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml
index b71a0346a..7b22b7f37 100644
--- a/infer/src/checkers/control.ml
+++ b/infer/src/checkers/control.ml
@@ -159,9 +159,9 @@ module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsContro
 
 type invariant_map = ControlDepAnalyzer.invariant_map
 
-let compute_invariant_map pdesc tenv control_maps : invariant_map =
-  let proc_data = ProcData.make pdesc tenv control_maps in
-  let node_cfg = CFG.from_pdesc pdesc in
+let compute_invariant_map summary tenv control_maps : invariant_map =
+  let proc_data = ProcData.make summary tenv control_maps in
+  let node_cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in
   ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:ControlDepSet.empty
 
 
diff --git a/infer/src/checkers/control.mli b/infer/src/checkers/control.mli
index 38c09857b..1213c2d18 100644
--- a/infer/src/checkers/control.mli
+++ b/infer/src/checkers/control.mli
@@ -26,7 +26,7 @@ type loop_control_maps =
   { exit_map: LoopHeads.t ExitNodeToLoopHeads.t
   ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t }
 
-val compute_invariant_map : Procdesc.t -> Tenv.t -> loop_control_maps -> invariant_map
+val compute_invariant_map : Summary.t -> Tenv.t -> loop_control_maps -> invariant_map
 
 val compute_control_vars :
      invariant_map
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index c15d0dfda..1645b137b 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -795,15 +795,15 @@ let report_errors proc_desc astate summary = Check.check_and_report astate proc_
 let checker {Callbacks.tenv; integer_type_widths; summary} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let inferbo_invariant_map =
-    BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths
+    BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
   in
   let node_cfg = NodeCFG.from_pdesc proc_desc in
   (* computes reaching defs: node -> (var -> node set) *)
-  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc tenv in
+  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map summary tenv in
   (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *)
   let control_maps, loop_head_to_loop_nodes = Loop_control.get_loop_control_maps node_cfg in
   (* computes the control dependencies: node -> var set *)
-  let control_dep_invariant_map = Control.compute_invariant_map proc_desc tenv control_maps in
+  let control_dep_invariant_map = Control.compute_invariant_map summary tenv control_maps in
   (* compute loop invariant map for control var analysis *)
   let loop_inv_map =
     let get_callee_purity callee_pname =
diff --git a/infer/src/checkers/functionPointers.ml b/infer/src/checkers/functionPointers.ml
index cb3211a06..05ebde1b8 100644
--- a/infer/src/checkers/functionPointers.ml
+++ b/infer/src/checkers/functionPointers.ml
@@ -90,13 +90,13 @@ let substitute_function_ptrs ~function_pointers node instr =
       instr
 
 
-let get_function_pointers proc_desc tenv =
-  let proc_data = ProcData.make_default proc_desc tenv in
-  let cfg = CFG.from_pdesc proc_desc in
+let get_function_pointers summary tenv =
+  let proc_data = ProcData.make_default summary tenv in
+  let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in
   Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty
 
 
-let substitute_function_pointers proc_desc tenv =
-  let function_pointers = get_function_pointers proc_desc tenv in
+let substitute_function_pointers summary tenv =
+  let function_pointers = get_function_pointers summary tenv in
   let f = substitute_function_ptrs ~function_pointers in
-  Procdesc.replace_instrs proc_desc ~f
+  Procdesc.replace_instrs (Summary.get_proc_desc summary) ~f
diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml
index d1eba58c4..f8abb4e19 100644
--- a/infer/src/checkers/hoisting.ml
+++ b/infer/src/checkers/hoisting.ml
@@ -153,12 +153,12 @@ let checker Callbacks.{tenv; summary; integer_type_widths} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let cfg = InstrCFG.from_pdesc proc_desc in
   (* computes reaching defs: node -> (var -> node set) *)
-  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc tenv in
+  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map summary tenv in
   let loop_head_to_source_nodes = Loop_control.get_loop_head_to_source_nodes cfg in
   let extract_cost_if_expensive =
     if Config.hoisting_report_only_expensive then
       let inferbo_invariant_map =
-        BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths
+        BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
       in
       let get_callee_cost_summary_and_formals callee_pname =
         Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname
diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml
index 91ab644c5..3eece9656 100644
--- a/infer/src/checkers/liveness.ml
+++ b/infer/src/checkers/liveness.ml
@@ -213,7 +213,7 @@ let get_captured_by_ref_invariant_map proc_desc proc_data =
 
 let checker {Callbacks.tenv; summary} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
-  let proc_data = ProcData.make_default proc_desc tenv in
+  let proc_data = ProcData.make_default summary tenv in
   let captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc proc_data in
   let cfg = CFG.from_pdesc proc_desc in
   let invariant_map = CheckerAnalyzer.exec_cfg cfg proc_data ~initial:Domain.empty in
diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml
index 94573f5ad..1b38ab346 100644
--- a/infer/src/checkers/purity.ml
+++ b/infer/src/checkers/purity.ml
@@ -211,14 +211,14 @@ let report_errors pdesc astate summary =
         proc_name
 
 
-let compute_summary proc_desc tenv get_callee_summary inferbo_invariant_map =
-  let proc_name = Procdesc.get_proc_name proc_desc in
+let compute_summary summary tenv get_callee_summary inferbo_invariant_map =
+  let proc_name = Summary.get_proc_name summary in
   let formals =
-    Procdesc.get_formals proc_desc
+    Procdesc.get_formals (Summary.get_proc_desc summary)
     |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name))
   in
   let proc_data =
-    ProcData.make proc_desc tenv {inferbo_invariant_map; formals; get_callee_summary}
+    ProcData.make summary tenv {inferbo_invariant_map; formals; get_callee_summary}
   in
   Analyzer.compute_post proc_data ~initial:PurityDomain.pure
 
@@ -226,10 +226,10 @@ let compute_summary proc_desc tenv get_callee_summary inferbo_invariant_map =
 let checker {Callbacks.tenv; summary; integer_type_widths} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let inferbo_invariant_map =
-    BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths
+    BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
   in
   let get_callee_summary = Payload.read proc_desc in
-  let astate = compute_summary proc_desc tenv get_callee_summary inferbo_invariant_map in
+  let astate = compute_summary summary tenv get_callee_summary inferbo_invariant_map in
   report_errors proc_desc astate summary ;
   match astate with
   | Some astate ->
diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml
index be2e4c97a..b351585d0 100644
--- a/infer/src/checkers/reachingDefs.ml
+++ b/infer/src/checkers/reachingDefs.ml
@@ -69,8 +69,9 @@ module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (No
 
 type invariant_map = Analyzer.invariant_map
 
-let compute_invariant_map pdesc tenv =
-  let proc_data = ProcData.make_default pdesc tenv in
+let compute_invariant_map summary tenv =
+  let pdesc = Summary.get_proc_desc summary in
+  let proc_data = ProcData.make_default summary tenv in
   let node_cfg = NodeCFG.from_pdesc pdesc in
   Analyzer.exec_cfg node_cfg proc_data ~initial:(init_reaching_defs_with_formals pdesc)
 
diff --git a/infer/src/checkers/reachingDefs.mli b/infer/src/checkers/reachingDefs.mli
index 20c6daa16..3ce0c383c 100644
--- a/infer/src/checkers/reachingDefs.mli
+++ b/infer/src/checkers/reachingDefs.mli
@@ -19,6 +19,6 @@ module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs)
 
 type invariant_map
 
-val compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map
+val compute_invariant_map : Summary.t -> Tenv.t -> invariant_map
 
 val extract_post : Procdesc.Node.id -> invariant_map -> ReachingDefsMap.t option
diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml
index f1ce1f7bd..21bacff73 100644
--- a/infer/src/checkers/uninit.ml
+++ b/infer/src/checkers/uninit.ml
@@ -179,8 +179,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  let exec_instr (astate : Domain.t) {ProcData.pdesc; extras= {formals; summary}; tenv} _
+  let exec_instr (astate : Domain.t) {ProcData.summary; extras= {formals}; tenv} _
       (instr : HilInstr.t) =
+    let pdesc = Summary.get_proc_desc summary in
     let check_access_expr ~loc rhs_access_expr =
       if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then
         report_intra rhs_access_expr loc summary
@@ -350,7 +351,7 @@ let checker {Callbacks.tenv; summary} : Summary.t =
   in
   let proc_data =
     let formals = FormalMap.make proc_desc in
-    ProcData.make proc_desc tenv {formals; summary}
+    ProcData.make summary tenv {formals; summary}
   in
   match Analyzer.compute_post proc_data ~initial with
   | Some {RecordDomain.prepost} ->
diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml
index e6fbcde22..bb0f0af7d 100644
--- a/infer/src/concurrency/RacerD.ml
+++ b/infer/src/concurrency/RacerD.ml
@@ -39,16 +39,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else
             let is_write = if List.is_empty access_list then is_write_access else false in
             let access = TraceElem.make_field_access prefix_path' ~is_write loc in
+            let pdesc = Summary.get_proc_desc proc_data.summary in
             match OwnershipDomain.get_owned prefix_path ownership with
             | OwnershipAbstractValue.OwnedIf formal_indexes ->
                 let pre =
                   AccessSnapshot.make access locks threads
-                    (AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes)
-                    proc_data.pdesc
+                    (AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes) pdesc
                 in
                 add_field_access pre
             | OwnershipAbstractValue.Unowned ->
-                let pre = AccessSnapshot.make access locks threads False proc_data.pdesc in
+                let pre = AccessSnapshot.make access locks threads False pdesc in
                 add_field_access pre )
     in
     List.fold (HilExp.get_access_exprs exp) ~init:accesses ~f:(fun acc access_expr ->
@@ -244,7 +244,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     else None
 
 
-  let treat_container_accesses ret_base callee_pname actuals loc {ProcData.tenv; pdesc} astate () =
+  let treat_container_accesses ret_base callee_pname actuals loc {ProcData.tenv; summary} astate ()
+      =
     let open RacerDModels in
     Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access ->
         match List.hd actuals with
@@ -253,18 +254,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let is_write =
               match container_access with ContainerWrite -> true | ContainerRead -> false
             in
-            make_container_access ret_base callee_pname ~is_write receiver_ap loc tenv pdesc astate
+            make_container_access ret_base callee_pname ~is_write receiver_ap loc tenv
+              (Summary.get_proc_desc summary) astate
         | _ ->
             L.internal_error "Call to %a is marked as a container write, but has no receiver"
               Typ.Procname.pp callee_pname ;
             None )
 
 
-  let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; pdesc}
+  let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary}
       (astate : Domain.t) () =
     let open Domain in
     let open RacerDModels in
     let open ConcurrencyModels in
+    let pdesc = Summary.get_proc_desc summary in
     let ret_access_path = (ret_base, []) in
     let astate =
       if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then
@@ -478,7 +481,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate' with accesses}
 
 
-  let exec_instr (astate : Domain.t) ({ProcData.pdesc} as proc_data) _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) ({ProcData.summary} as proc_data) _ (instr : HilInstr.t) =
     match instr with
     | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
         let astate = add_reads actuals loc astate proc_data in
@@ -488,7 +491,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         |> IOption.if_none_eval
              ~f:(do_proc_call ret_base callee_pname actuals call_flags loc proc_data astate)
     | Call (_, Indirect _, _, _, _) ->
-        if Typ.Procname.is_java (Procdesc.get_proc_name pdesc) then
+        if Typ.Procname.is_java (Summary.get_proc_name summary) then
           L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr
         else astate
     | Assign (lhs_access_expr, rhs_exp, loc) ->
@@ -515,7 +518,7 @@ let analyze_procedure {Callbacks.tenv; summary} =
   let open RacerDDomain in
   if should_analyze_proc proc_desc tenv then
     let formal_map = FormalMap.make proc_desc in
-    let proc_data = ProcData.make proc_desc tenv ProcData.empty_extras in
+    let proc_data = ProcData.make summary tenv ProcData.empty_extras in
     let initial =
       let threads =
         if
diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml
index 1c43e7083..ef907fee5 100644
--- a/infer/src/concurrency/starvation.ml
+++ b/infer/src/concurrency/starvation.ml
@@ -52,7 +52,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = FormalMap.t
 
-  let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv; extras} _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) {ProcData.summary; tenv; extras} _ (instr : HilInstr.t) =
     let open ConcurrencyModels in
     let open StarvationModels in
     let log_parse_error error pname actuals =
@@ -75,13 +75,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | _ ->
           None
     in
-    let is_java = Procdesc.get_proc_name pdesc |> Typ.Procname.is_java in
+    let is_java = Summary.get_proc_name summary |> Typ.Procname.is_java in
     let do_lock locks loc astate =
       List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate loc
     in
     let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in
     let do_call callee loc astate =
-      Payload.read pdesc callee
+      Payload.read (Summary.get_proc_desc summary) callee
       |> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc)
     in
     match instr with
@@ -141,7 +141,7 @@ let analyze_procedure {Callbacks.tenv; summary} =
   if StarvationModels.should_skip_analysis tenv pname [] then summary
   else
     let formals = FormalMap.make proc_desc in
-    let proc_data = ProcData.make proc_desc tenv formals in
+    let proc_data = ProcData.make summary tenv formals in
     let loc = Procdesc.get_loc proc_desc in
     let initial =
       if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.bottom
diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml
index a5d33c828..086db5b14 100644
--- a/infer/src/labs/ResourceLeaks.ml
+++ b/infer/src/labs/ResourceLeaks.ml
@@ -53,7 +53,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   (** Take an abstract state and instruction, produce a new abstract state *)
-  let exec_instr (astate : ResourceLeakDomain.t) {ProcData.pdesc= _; tenv= _} _
+  let exec_instr (astate : ResourceLeakDomain.t) {ProcData.summary= _; tenv= _} _
       (instr : HilInstr.t) =
     match instr with
     | Call (_return_opt, Direct _callee_procname, _actuals, _, _loc) ->
@@ -87,7 +87,7 @@ let report_if_leak _post _summary (_proc_data : unit ProcData.t) = ()
 
 (* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
 let checker {Callbacks.summary; tenv} : Summary.t =
-  let proc_data = ProcData.make (Summary.get_proc_desc summary) tenv () in
+  let proc_data = ProcData.make summary tenv () in
   match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with
   | Some post ->
       report_if_leak post summary proc_data ;
@@ -95,4 +95,4 @@ let checker {Callbacks.summary; tenv} : Summary.t =
   | None ->
       L.(die InternalError)
         "Analyzer failed to compute post for %a" Typ.Procname.pp
-        (Procdesc.get_proc_name proc_data.pdesc)
+        (Summary.get_proc_name proc_data.summary)
diff --git a/infer/src/nullsafe/NullabilityCheck.ml b/infer/src/nullsafe/NullabilityCheck.ml
index b350975db..611bb66e3 100644
--- a/infer/src/nullsafe/NullabilityCheck.ml
+++ b/infer/src/nullsafe/NullabilityCheck.ml
@@ -18,7 +18,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = Summary.t
+  type extras = unit
 
   let rec is_pointer_subtype tenv typ1 typ2 =
     match (typ1.Typ.desc, typ2.Typ.desc) with
@@ -97,11 +97,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         Option.map ~f:Procdesc.get_attributes (Ondemand.get_proc_desc pname)
 
 
-  let report_nullable_dereference ap call_sites {ProcData.pdesc; extras} loc =
-    let summary = extras in
+  let report_nullable_dereference ap call_sites {ProcData.summary} loc =
     if is_conflicting_report summary loc then ()
     else
-      let pname = Procdesc.get_proc_name pdesc in
+      let pname = Summary.get_proc_name summary in
       let annotation = Localise.nullable_annotation_name pname in
       let call_site =
         try CallSites.min_elt call_sites
@@ -339,6 +338,6 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.E
 
 let checker {Callbacks.summary; tenv} =
   let initial = (NullableAP.empty, NullCheckedPname.empty) in
-  let proc_data = ProcData.make (Summary.get_proc_desc summary) tenv summary in
+  let proc_data = ProcData.make summary tenv () in
   ignore (Analyzer.compute_post proc_data ~initial) ;
   summary
diff --git a/infer/src/nullsafe/NullabilitySuggest.ml b/infer/src/nullsafe/NullabilitySuggest.ml
index aecb1e1ae..bec8ff99c 100644
--- a/infer/src/nullsafe/NullabilitySuggest.ml
+++ b/infer/src/nullsafe/NullabilitySuggest.ml
@@ -159,7 +159,7 @@ let make_error_trace astate ap ud =
 
 
 let pretty_field_name proc_data field_name =
-  match Procdesc.get_proc_name proc_data.ProcData.pdesc with
+  match Summary.get_proc_name proc_data.ProcData.summary with
   | Typ.Procname.Java jproc_name ->
       let proc_class_name = Typ.Procname.Java.get_class_name jproc_name in
       let field_class_name = Typ.Fieldname.Java.get_class field_name in
@@ -218,7 +218,7 @@ let checker {Callbacks.summary; tenv} =
   else
     (* Assume all fields are not null in the beginning *)
     let initial = Domain.empty in
-    let proc_data = ProcData.make_default proc_desc tenv in
+    let proc_data = ProcData.make_default summary tenv in
     ( match Analyzer.compute_post proc_data ~initial with
     | Some post ->
         report post proc_data
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index b2b1d2392..8f11e1036 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -52,7 +52,7 @@ module PulseTransferFunctions = struct
   module CFG = ProcCfg.Exceptional
   module Domain = PulseAbductiveDomain
 
-  type extras = Summary.t
+  type extras = unit
 
   let exec_unknown_call reason ret call actuals _flags call_loc astate =
     let event = ValueHistory.Call {f= reason; location= call_loc} in
@@ -154,7 +154,7 @@ module PulseTransferFunctions = struct
             posts )
 
 
-  let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : Sil.instr) =
+  let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) =
     match instr with
     | Load (lhs_id, rhs_exp, _typ, loc) ->
         (* [lhs_id := *rhs_exp] *)
@@ -215,11 +215,11 @@ module DisjunctiveTransferFunctions =
 module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFunctions)
 
 let checker {Callbacks.tenv; summary} =
-  let proc_desc = Summary.get_proc_desc summary in
-  let proc_data = ProcData.make proc_desc tenv summary in
+  let proc_data = ProcData.make summary tenv () in
   AbstractAddress.init () ;
   let initial =
-    DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial proc_desc)
+    DisjunctiveTransferFunctions.Disjuncts.singleton
+      (PulseAbductiveDomain.mk_initial (Summary.get_proc_desc summary))
   in
   match DisjunctiveAnalyzer.compute_post proc_data ~initial with
   | Some posts ->
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 7bb42a3dd..6c7d05d13 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -124,11 +124,11 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     let report_trace ?(sink_indexes = IntSet.empty) trace cur_site (proc_data : extras ProcData.t)
         =
       let get_summary pname =
-        if Typ.Procname.equal pname (Procdesc.get_proc_name proc_data.pdesc) then
+        if Typ.Procname.equal pname (Summary.get_proc_name proc_data.summary) then
           (* read_summary will trigger ondemand analysis of the current proc. we don't want that. *)
           TaintDomain.bottom
         else
-          match Payload.read proc_data.pdesc pname with
+          match Payload.read (Summary.get_proc_desc proc_data.summary) pname with
           | Some summary ->
               TaintSpecification.of_summary_access_tree summary
           | None ->
@@ -473,7 +473,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       if Var.is_global var then
         let dummy_call_site = CallSite.make BuiltinDecl.__global_access loc in
         let sources =
-          let caller_pname = Procdesc.get_proc_name proc_data.ProcData.pdesc in
+          let caller_pname = Summary.get_proc_name proc_data.ProcData.summary in
           TraceDomain.Source.get ~caller_pname dummy_call_site
             [HilExp.AccessExpression access_expr]
             proc_data.tenv
@@ -642,7 +642,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       in
       let astate_with_direct_sources =
         let sources =
-          let caller_pname = Procdesc.get_proc_name proc_data.ProcData.pdesc in
+          let caller_pname = Summary.get_proc_name proc_data.ProcData.summary in
           TraceDomain.Source.get ~caller_pname call_site actuals proc_data.tenv
         in
         List.fold sources ~init:astate_with_sink
@@ -655,7 +655,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 add_actual_source source index actuals astate_with_sink proc_data )
       in
       let astate_with_summary =
-        match Payload.read proc_data.pdesc callee_pname with
+        match Payload.read (Summary.get_proc_desc proc_data.summary) callee_pname with
         | None ->
             handle_unknown_call callee_pname astate_with_direct_sources
         | Some summary -> (
@@ -697,7 +697,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           astate
       | Assign (Base (Var.ProgramVar pvar, _), rhs_exp, _)
         when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp
-             && Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc ->
+             && Typ.equal_desc Tvoid
+                  (Procdesc.get_ret_type (Summary.get_proc_desc proc_data.summary)).desc ->
           (* similar to the case above; the Java frontend translates "return no exception" as
              `return null` in a void function *)
           astate
@@ -770,8 +771,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       access_tree
 
 
-  let make_summary {ProcData.pdesc; extras= {formal_map}} access_tree =
-    let is_java = Typ.Procname.is_java (Procdesc.get_proc_name pdesc) in
+  let make_summary {ProcData.summary; extras= {formal_map}} access_tree =
+    let is_java = Typ.Procname.is_java (Summary.get_proc_name summary) in
     (* if a trace has footprint sources, attach them to the appropriate footprint var *)
     let access_tree' =
       TaintDomain.fold
@@ -868,7 +869,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       let formal_map = FormalMap.make proc_desc in
       {formal_map; summary}
     in
-    let proc_data = ProcData.make proc_desc tenv extras in
+    let proc_data = ProcData.make summary tenv extras in
     match Analyzer.compute_post proc_data ~initial with
     | Some access_tree ->
         Payload.update_summary (make_summary proc_data access_tree) summary
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 17e55afdd..b3bb237d5 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -243,13 +243,13 @@ struct
     let exit_node = create_node Procdesc.Node.Exit_node [] in
     set_succs last_node [exit_node] ~exn_handlers:no_exn_handlers ;
     Procdesc.set_exit_node pdesc exit_node ;
-    (pdesc, assert_map)
+    (Summary.reset pdesc, assert_map)
 
 
   let create_test test_program extras ~initial pp_opt test_pname _ =
     let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in
-    let pdesc, assert_map = structured_program_to_cfg test_program test_pname in
-    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) ~initial in
+    let summary, assert_map = structured_program_to_cfg test_program test_pname in
+    let inv_map = I.exec_pdesc (ProcData.make summary (Tenv.create ()) extras) ~initial in
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =
         try