diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml
index 1ff623aa0..03f3ec73f 100644
--- a/infer/src/absint/AbstractInterpreter.ml
+++ b/infer/src/absint/AbstractInterpreter.ml
@@ -17,19 +17,19 @@ module VisitCount : sig
 
   val first_time : t
 
-  val succ : pdesc:Procdesc.t -> t -> t
+  val succ : t -> t
 end = struct
   type t = int
 
   let first_time = 1
 
-  let succ ~pdesc visit_count =
+  let succ visit_count =
     let visit_count' = visit_count + 1 in
     if visit_count' > Config.max_widens then
-      L.(die InternalError)
-        "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
-         operator or increase the threshold"
-        Config.max_widens Procname.pp (Procdesc.get_proc_name pdesc) ;
+      L.die InternalError
+        "Exceeded max widening threshold %d. Please check your widening operator or increase the \
+         threshold"
+        Config.max_widens ;
     visit_count'
 end
 
@@ -56,21 +56,23 @@ module type S = sig
   val compute_post :
        ?do_narrowing:bool
     -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option)
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
+    -> Procdesc.t
     -> TransferFunctions.Domain.t option
 
   val exec_cfg :
        ?do_narrowing:bool
     -> TransferFunctions.CFG.t
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
     -> invariant_map
 
   val exec_pdesc :
        ?do_narrowing:bool
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
+    -> Procdesc.t
     -> invariant_map
 
   val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
@@ -112,7 +114,7 @@ module MakeDisjunctiveTransferFunctions
 struct
   module CFG = T.CFG
 
-  type extras = T.extras
+  type analysis_data = T.analysis_data
 
   module Domain = struct
     (** a list [\[x1; x2; ...; xN\]] represents a disjunction [x1 ∨ x2 ∨ ... ∨ xN] *)
@@ -180,10 +182,10 @@ struct
       F.fprintf f "@[<v>%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts
   end
 
-  let exec_instr pre_disjuncts extras node instr =
+  let exec_instr pre_disjuncts analysis_data node instr =
     List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct ->
         L.d_printfln "@[<v2>Executing instruction from disjunct #%d@;" i ;
-        let disjuncts' = T.exec_instr pre_disjunct extras node instr in
+        let disjuncts' = T.exec_instr pre_disjunct analysis_data node instr in
         ( if Config.write_html then
           let n = List.length disjuncts' in
           L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ;
@@ -315,17 +317,16 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = 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.summary} as proc_data) node ~is_loop_head ~is_narrowing
-      astate_pre inv_map =
+  let exec_node ~pp_instr analysis_data node ~is_loop_head ~is_narrowing astate_pre inv_map =
     let node_id = Node.id node in
     let update_inv_map inv_map new_pre old_state_opt =
-      let new_post = exec_node_instrs old_state_opt ~pp_instr proc_data node new_pre in
+      let new_post = exec_node_instrs old_state_opt ~pp_instr analysis_data node new_pre in
       let new_visit_count =
         match old_state_opt with
         | None ->
             VisitCount.first_time
         | Some {State.visit_count; _} ->
-            VisitCount.succ ~pdesc:(Summary.get_proc_desc summary) visit_count
+            VisitCount.succ visit_count
       in
       InvariantMap.add node_id
         {State.pre= new_pre; post= new_post; visit_count= new_visit_count}
@@ -351,9 +352,8 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
           else Domain.leq ~lhs:new_pre ~rhs:old_state.State.pre
         then (inv_map, ReachedFixPoint)
         else if is_narrowing && not (Domain.leq ~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@."
-            Procname.pp (Summary.get_proc_name summary) Node.pp_id node_id ;
+          L.d_printfln "Terminate narrowing because old and new states are not comparable: %a@."
+            Node.pp_id node_id ;
           (inv_map, ReachedFixPoint) )
         else (update_inv_map inv_map new_pre (Some old_state), DidNotReachFixPoint)
       else
@@ -401,17 +401,16 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s
 
 
   (** compute and return an invariant map for [pdesc] *)
-  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
+  let make_exec_pdesc ~exec_cfg_internal analysis_data ~do_narrowing ~initial proc_desc =
+    exec_cfg_internal ~pp_instr:pp_sil_instr (CFG.from_pdesc proc_desc) analysis_data ~do_narrowing
+      ~initial
 
 
   (** compute and return the postcondition of [pdesc] *)
-  let make_compute_post ~exec_cfg_internal ?(pp_instr = pp_sil_instr)
-      ({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
+  let make_compute_post ~exec_cfg_internal ?(pp_instr = pp_sil_instr) analysis_data ~do_narrowing
+      ~initial proc_desc =
+    let cfg = CFG.from_pdesc proc_desc in
+    let inv_map = exec_cfg_internal ~pp_instr cfg analysis_data ~do_narrowing ~initial in
     extract_post (Node.id (CFG.exit_node cfg)) inv_map
 end
 
@@ -421,17 +420,17 @@ module MakeWithScheduler
 struct
   include AbstractInterpreterCommon (SimpleNodeTransferFunctions (TransferFunctions))
 
-  let rec exec_worklist ~pp_instr cfg ({ProcData.summary} as proc_data) work_queue inv_map =
+  let rec exec_worklist ~pp_instr cfg analysis_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
+        exec_worklist ~pp_instr cfg analysis_data work_queue' inv_map
     | Some (node, _, work_queue') ->
         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 (Summary.get_proc_desc summary) node in
+              let is_loop_head = CFG.is_loop_head (CFG.proc_desc cfg) node in
               match
-                exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing:false astate_pre
+                exec_node ~pp_instr analysis_data node ~is_loop_head ~is_narrowing:false astate_pre
                   inv_map
               with
               | inv_map, ReachedFixPoint ->
@@ -441,20 +440,20 @@ struct
           | None ->
               (inv_map, work_queue')
         in
-        exec_worklist ~pp_instr cfg proc_data work_queue_post inv_map_post
+        exec_worklist ~pp_instr cfg analysis_data work_queue_post inv_map_post
     | None ->
         inv_map
 
 
   (** compute and return an invariant map for [cfg] *)
-  let exec_cfg_internal ~pp_instr cfg proc_data ~do_narrowing:_ ~initial =
+  let exec_cfg_internal ~pp_instr cfg analysis_data ~do_narrowing:_ ~initial =
     let start_node = CFG.start_node cfg in
     let inv_map, _did_not_reach_fix_point =
-      exec_node ~pp_instr proc_data start_node ~is_loop_head:false ~is_narrowing:false initial
+      exec_node ~pp_instr analysis_data start_node ~is_loop_head:false ~is_narrowing:false initial
         InvariantMap.empty
     in
     let work_queue = Scheduler.schedule_succs (Scheduler.empty cfg) start_node in
-    exec_worklist ~pp_instr cfg proc_data work_queue inv_map
+    exec_worklist ~pp_instr cfg analysis_data work_queue inv_map
 
 
   let exec_cfg ?do_narrowing:_ = exec_cfg_internal ~pp_instr:pp_sil_instr ~do_narrowing:false
diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli
index cd2eabe9e..aa0d2c844 100644
--- a/infer/src/absint/AbstractInterpreter.mli
+++ b/infer/src/absint/AbstractInterpreter.mli
@@ -27,24 +27,26 @@ module type S = sig
   val compute_post :
        ?do_narrowing:bool
     -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option)
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
+    -> Procdesc.t
     -> TransferFunctions.Domain.t option
-  (** compute and return the postcondition for the given procedure starting from [initial].
+  (** compute and return the postcondition for the given {Procdesc.t} starting from [initial].
       [pp_instr] is used for the debug HTML and passed as a hook to handle both SIL and HIL CFGs. *)
 
   val exec_cfg :
        ?do_narrowing:bool
     -> TransferFunctions.CFG.t
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
     -> invariant_map
   (** compute and return invariant map for the given CFG/procedure starting from [initial]. *)
 
   val exec_pdesc :
        ?do_narrowing:bool
-    -> TransferFunctions.extras ProcData.t
+    -> TransferFunctions.analysis_data
     -> initial:TransferFunctions.Domain.t
+    -> Procdesc.t
     -> invariant_map
   (** compute and return invariant map for the given procedure starting from [initial] *)
 
@@ -77,6 +79,6 @@ module MakeDisjunctive
     (T : TransferFunctions.DisjReady)
     (DConfig : TransferFunctions.DisjunctiveConfig) :
   S
-    with type TransferFunctions.extras = T.extras
+    with type TransferFunctions.analysis_data = T.analysis_data
      and module TransferFunctions.CFG = T.CFG
      and type TransferFunctions.Domain.t = T.Domain.t list
diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml
index 8bec0e209..d6da320ee 100644
--- a/infer/src/absint/LowerHil.ml
+++ b/infer/src/absint/LowerHil.ml
@@ -30,7 +30,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
   module CFG = TransferFunctions.CFG
   module Domain = MakeHILDomain (TransferFunctions.Domain)
 
-  type extras = TransferFunctions.extras
+  type analysis_data = TransferFunctions.analysis_data
 
   let pp_session_name = TransferFunctions.pp_session_name
 
@@ -40,7 +40,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
     && match ConcurrencyModels.get_lock_effect pname actuals with Unlock _ -> true | _ -> false
 
 
-  let exec_instr_actual extras bindings node hil_instr actual_state =
+  let exec_instr_actual analysis_data bindings node hil_instr actual_state =
     match (hil_instr : HilInstr.t) with
     | Call (_, Direct callee_pname, actuals, _, loc) as hil_instr
       when is_java_unlock callee_pname actuals ->
@@ -53,11 +53,11 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
               let dummy_assign =
                 HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc)
               in
-              TransferFunctions.exec_instr astate_acc extras node dummy_assign )
+              TransferFunctions.exec_instr astate_acc analysis_data node dummy_assign )
         in
-        (TransferFunctions.exec_instr actual_state' extras node hil_instr, Bindings.empty)
+        (TransferFunctions.exec_instr actual_state' analysis_data node hil_instr, Bindings.empty)
     | hil_instr ->
-        (TransferFunctions.exec_instr actual_state extras node hil_instr, bindings)
+        (TransferFunctions.exec_instr actual_state analysis_data node hil_instr, bindings)
 
 
   let append_bindings = IList.append_no_duplicates ~cmp:Var.compare |> Staged.unstage
@@ -84,13 +84,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
         (Some instr, bindings)
 
 
-  let exec_instr ((actual_state, bindings) as astate) extras node instr =
+  let exec_instr ((actual_state, bindings) as astate) analysis_data node instr =
     let actual_state', bindings' =
       match hil_instr_of_sil bindings instr with
       | None, bindings ->
           (actual_state, bindings)
       | Some hil_instr, bindings ->
-          exec_instr_actual extras bindings node hil_instr actual_state
+          exec_instr_actual analysis_data bindings node hil_instr actual_state
     in
     if phys_equal bindings bindings' && phys_equal actual_state actual_state' then astate
     else (actual_state', bindings')
@@ -102,7 +102,7 @@ module type S = sig
   type domain
 
   val compute_post :
-    Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option
+    Interpreter.TransferFunctions.analysis_data -> initial:domain -> Procdesc.t -> domain option
 end
 
 module MakeAbstractInterpreterWithConfig
@@ -117,7 +117,7 @@ module MakeAbstractInterpreterWithConfig
 
   type domain = TransferFunctions.Domain.t
 
-  let compute_post proc_data ~initial =
+  let compute_post analysis_data ~initial proc_desc =
     let initial' = (initial, Bindings.empty) in
     let pp_instr (_, bindings) instr =
       match LowerHilInterpreter.hil_instr_of_sil bindings instr with
@@ -126,7 +126,8 @@ module MakeAbstractInterpreterWithConfig
       | None, _ ->
           None
     in
-    Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst
+    Interpreter.compute_post ~pp_instr analysis_data ~initial:initial' proc_desc
+    |> Option.map ~f:fst
 end
 
 module MakeAbstractInterpreter (TransferFunctions : TransferFunctions.HIL) =
diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli
index 9c6a4093d..bf1407a8e 100644
--- a/infer/src/absint/LowerHil.mli
+++ b/infer/src/absint/LowerHil.mli
@@ -27,9 +27,9 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
 
   module Domain : module type of AbstractDomain.Pair (TransferFunctions.Domain) (Bindings)
 
-  type extras = TransferFunctions.extras
+  type analysis_data = TransferFunctions.analysis_data
 
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t
+  val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
@@ -40,7 +40,7 @@ module type S = sig
   type domain
 
   val compute_post :
-    Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option
+    Interpreter.TransferFunctions.analysis_data -> initial:domain -> Procdesc.t -> domain option
   (** compute and return the postcondition for the given procedure starting from [initial]. *)
 end
 
diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml
index b315ca025..6f79c860d 100644
--- a/infer/src/absint/TransferFunctions.ml
+++ b/infer/src/absint/TransferFunctions.ml
@@ -12,11 +12,11 @@ module type S = sig
 
   module Domain : AbstractDomain.S
 
-  type extras
+  type analysis_data
 
   type instr
 
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t
+  val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
@@ -44,9 +44,9 @@ module type DisjReady = sig
 
   module Domain : AbstractDomain.NoJoin
 
-  type extras
+  type analysis_data
 
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list
+  val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli
index 67da62eb1..3b86b3e83 100644
--- a/infer/src/absint/TransferFunctions.mli
+++ b/infer/src/absint/TransferFunctions.mli
@@ -17,12 +17,12 @@ module type S = sig
   (** abstract domain whose state we propagate *)
 
   (** read-only extra state (results of previous analyses, globals, etc.) *)
-  type extras
+  type analysis_data
 
   (** type of the instructions the transfer functions operate on *)
   type instr
 
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t
+  val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t
   (** [exec_instr astate proc_data node instr] should usually return [astate'] such that
       [{astate} instr {astate'}] is a valid Hoare triple. In other words, [exec_instr] defines how
       executing an instruction from a given abstract state changes that state into a new one. This
@@ -57,9 +57,9 @@ module type DisjReady = sig
 
   module Domain : AbstractDomain.NoJoin
 
-  type extras
+  type analysis_data
 
-  val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list
+  val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t list
 
   val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
diff --git a/infer/src/absint/ProcData.ml b/infer/src/backend/ProcData.ml
similarity index 61%
rename from infer/src/absint/ProcData.ml
rename to infer/src/backend/ProcData.ml
index 06a675afe..57aa63fdf 100644
--- a/infer/src/absint/ProcData.ml
+++ b/infer/src/backend/ProcData.ml
@@ -8,11 +8,3 @@
 open! IStd
 
 type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a}
-
-type no_extras = unit
-
-let empty_extras = ()
-
-let make summary tenv extras = {summary; tenv; extras}
-
-let make_default summary tenv = make summary tenv empty_extras
diff --git a/infer/src/absint/ProcData.mli b/infer/src/backend/ProcData.mli
similarity index 63%
rename from infer/src/absint/ProcData.mli
rename to infer/src/backend/ProcData.mli
index 743f93f22..57aa63fdf 100644
--- a/infer/src/absint/ProcData.mli
+++ b/infer/src/backend/ProcData.mli
@@ -8,11 +8,3 @@
 open! IStd
 
 type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a}
-
-type no_extras
-
-val empty_extras : no_extras
-
-val make : Summary.t -> Tenv.t -> 'a -> 'a t
-
-val make_default : Summary.t -> Tenv.t -> no_extras t
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index 14382a4ac..5f20b7fa1 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
@@ -58,7 +58,7 @@ module TransferFunctions = struct
   module CFG = CFG
   module Domain = Dom.Mem
 
-  type nonrec extras = extras
+  type analysis_data = extras ProcData.t
 
   let instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location mem =
     match
@@ -455,10 +455,10 @@ let compute_invariant_map :
   let cfg = CFG.from_pdesc pdesc in
   let pdata =
     let oenv = OndemandEnv.mk pdesc tenv integer_type_widths in
-    ProcData.make summary tenv {get_summary; get_formals; oenv}
+    {ProcData.summary; tenv; extras= {get_summary; get_formals; oenv}}
   in
   let initial = Init.initial_state pdata (CFG.start_node cfg) in
-  Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata
+  Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata pdesc
 
 
 let cached_compute_invariant_map =
diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml
index f3287d8e7..ebf86b1e7 100644
--- a/infer/src/checkers/NullabilityPreanalysis.ml
+++ b/infer/src/checkers/NullabilityPreanalysis.ml
@@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = FieldsAssignedInConstructors
 
-  type extras = Exp.t Ident.Hash.t
+  type analysis_data = Exp.t Ident.Hash.t ProcData.t
 
   let exp_is_null ids_map exp =
     match exp with
@@ -95,7 +95,8 @@ let analysis cfg tenv =
     if Procdesc.is_defined pdesc && Procname.is_constructor proc_name then
       match
         FieldsAssignedInConstructorsChecker.compute_post ~initial
-          (ProcData.make (Summary.OnDisk.reset pdesc) tenv (Ident.Hash.create 10))
+          {ProcData.summary= Summary.OnDisk.reset pdesc; tenv; extras= Ident.Hash.create 10}
+          pdesc
       with
       | Some new_domain ->
           FieldsAssignedInConstructors.union new_domain domain
diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml
index 67cc57871..8c7f1018b 100644
--- a/infer/src/checkers/RequiredProps.ml
+++ b/infer/src/checkers/RequiredProps.ml
@@ -205,6 +205,8 @@ module TransferFunctions = struct
 
   type extras = {get_proc_summary_and_formals: get_proc_summary_and_formals}
 
+  type analysis_data = extras ProcData.t
+
   let apply_callee_summary summary_opt callsite ~caller_pname ~callee_pname ret_id_typ formals
       actuals astate =
     Option.value_map summary_opt ~default:astate ~f:(fun callee_summary ->
@@ -291,21 +293,21 @@ let init_extras summary =
     |> Option.map ~f:(fun (callee_pdesc, callee_summary) ->
            (callee_summary, Procdesc.get_pvar_formals callee_pdesc) )
   in
-  TransferFunctions.{get_proc_summary_and_formals}
+  {TransferFunctions.get_proc_summary_and_formals}
 
 
 let checker {Callbacks.summary; exe_env} =
   let proc_desc = Summary.get_proc_desc summary in
   let proc_name = Summary.get_proc_name summary in
   let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
-  let proc_data = ProcData.make summary tenv (init_extras summary) in
+  let proc_data = {ProcData.summary; tenv; extras= init_extras summary} in
   let ret_path =
     let ret_var = Procdesc.get_ret_var proc_desc in
     let ret_typ = Procdesc.get_ret_type proc_desc in
     Domain.LocalAccessPath.make_from_pvar ret_var ret_typ proc_name
   in
   let initial = Domain.init tenv proc_name (Procdesc.get_pvar_formals proc_desc) ret_path in
-  match Analyzer.compute_post proc_data ~initial with
+  match Analyzer.compute_post proc_data ~initial proc_desc with
   | Some post ->
       let is_void_func = Procdesc.get_ret_type proc_desc |> Typ.is_void in
       let post = Domain.get_summary ~is_void_func post in
diff --git a/infer/src/checkers/SelfInBlock.ml b/infer/src/checkers/SelfInBlock.ml
index 90866f6b6..9e7b936e3 100644
--- a/infer/src/checkers/SelfInBlock.ml
+++ b/infer/src/checkers/SelfInBlock.ml
@@ -143,7 +143,7 @@ module TransferFunctions = struct
   module Domain = Domain
   module CFG = ProcCfg.Normal
 
-  type extras = unit
+  type analysis_data = unit ProcData.t
 
   let pp_session_name _node fmt = F.pp_print_string fmt "SelfCapturedInBlock"
 
@@ -555,10 +555,10 @@ let checker {Callbacks.exe_env; summary} =
   let initial = {Domain.vars= Vars.empty; strongVars= StrongEqualToWeakCapturedVars.empty} in
   let procname = Summary.get_proc_name summary in
   let tenv = Exe_env.get_tenv exe_env procname in
-  let proc_data = ProcData.make summary tenv () in
+  let proc_data = {ProcData.summary; tenv; extras= ()} in
   let attributes = Summary.get_attributes summary in
   ( if Procname.is_objc_block procname then
-    match Analyzer.compute_post proc_data ~initial with
+    match Analyzer.compute_post proc_data ~initial (Summary.get_proc_desc summary) with
     | Some domain ->
         report_issues summary domain.vars attributes
     | None ->
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
index 797ad5757..295bf744e 100644
--- a/infer/src/checkers/SimpleChecker.ml
+++ b/infer/src/checkers/SimpleChecker.ml
@@ -60,7 +60,7 @@ module Make (Spec : Spec) : S = struct
     module CFG = CFG
     module Domain = Domain
 
-    type extras = ProcData.no_extras
+    type analysis_data = unit ProcData.t
 
     let exec_instr astate_set proc_data node instr =
       let node_kind = CFG.Node.kind node in
@@ -94,7 +94,9 @@ 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 summary tenv) ~initial:Domain.empty in
+    let inv_map =
+      Analyzer.exec_pdesc {ProcData.summary; tenv; extras= ()} ~initial:Domain.empty proc_desc
+    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 6772021e2..ab11d3431 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -66,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = SiofDomain
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   let is_compile_time_constructed summary pv =
     let init_pname = Pvar.get_initializer_pname pv in
@@ -287,7 +287,7 @@ let checker {Callbacks.exe_env; summary} : Summary.t =
     in
     includes_iostream (Procdesc.get_attributes proc_desc).ProcAttributes.translation_unit
   in
-  let proc_data = ProcData.make_default summary tenv in
+  let proc_data = {ProcData.summary; tenv; extras= ()} in
   let initial =
     ( Bottom
     , if standard_streams_initialized_in_tu then SiofDomain.VarNames.of_list standard_streams
@@ -302,7 +302,7 @@ let checker {Callbacks.exe_env; summary} : Summary.t =
       match pname with ObjC_Cpp cpp_pname -> Procname.ObjC_Cpp.is_constexpr cpp_pname | _ -> false
     then Payload.update_summary initial summary
     else
-      match Analyzer.compute_post proc_data ~initial with
+      match Analyzer.compute_post proc_data ~initial proc_desc with
       | Some post ->
           Payload.update_summary post summary
       | None ->
diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml
index f99d2c131..98955498d 100644
--- a/infer/src/checkers/addressTaken.ml
+++ b/infer/src/checkers/addressTaken.ml
@@ -17,7 +17,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   let rec add_address_taken_pvars exp astate =
     match exp with
diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml
index 5473cdbfa..bdfc9a3f7 100644
--- a/infer/src/checkers/annotationReachability.ml
+++ b/infer/src/checkers/annotationReachability.ml
@@ -485,7 +485,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = AnnotationSpec.t list
+  type analysis_data = AnnotationSpec.t list ProcData.t
 
   let is_sink tenv (spec : AnnotationSpec.t) ~caller_pname ~callee_pname =
     spec.sink_predicate tenv callee_pname
@@ -548,8 +548,8 @@ let checker ({Callbacks.exe_env; summary} as callback) : Summary.t =
   let tenv = Exe_env.get_tenv exe_env proc_name in
   let initial = Domain.empty in
   let specs = get_annot_specs proc_name in
-  let proc_data = ProcData.make summary tenv specs in
-  match Analyzer.compute_post proc_data ~initial with
+  let proc_data = {ProcData.summary; tenv; extras= specs} in
+  match Analyzer.compute_post proc_data ~initial (Summary.get_proc_desc summary) with
   | Some annot_map ->
       List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report callback annot_map) ;
       Payload.update_summary annot_map summary
diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml
index b99b4713b..ee86963d9 100644
--- a/infer/src/checkers/control.ml
+++ b/infer/src/checkers/control.ml
@@ -56,7 +56,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ControlDepSet
 
-  type extras = loop_control_maps
+  type analysis_data = loop_control_maps ProcData.t
 
   let collect_vars_in_exp exp loop_head =
     Var.get_all_vars_in_exp exp
@@ -160,7 +160,7 @@ module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsContro
 type invariant_map = ControlDepAnalyzer.invariant_map
 
 let compute_invariant_map summary tenv control_maps : invariant_map =
-  let proc_data = ProcData.make summary tenv control_maps in
+  let proc_data = {ProcData.summary; tenv; extras= 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/functionPointers.ml b/infer/src/checkers/functionPointers.ml
index c6bde9bac..ce4adf993 100644
--- a/infer/src/checkers/functionPointers.ml
+++ b/infer/src/checkers/functionPointers.ml
@@ -21,7 +21,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   let exec_instr astate _ _ = function
     | Sil.Load {id= lhs_id} when Ident.is_none lhs_id ->
@@ -91,7 +91,7 @@ let substitute_function_ptrs ~function_pointers node instr =
 
 
 let get_function_pointers summary tenv =
-  let proc_data = ProcData.make_default summary tenv in
+  let proc_data = {ProcData.summary; tenv; extras= ()} in
   let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in
   Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty
 
diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml
index 7cc469c06..ea0201ebc 100644
--- a/infer/src/checkers/liveness.ml
+++ b/infer/src/checkers/liveness.ml
@@ -92,7 +92,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   (** add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
@@ -181,7 +181,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = VarSet
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   let exec_instr astate _ _ instr =
     List.fold (Sil.exps_of_instr instr)
@@ -213,7 +213,7 @@ let get_captured_by_ref_invariant_map proc_desc proc_data =
 let checker {Callbacks.exe_env; summary} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
-  let proc_data = ProcData.make_default summary tenv in
+  let proc_data = {ProcData.summary; tenv; extras= ()} 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/liveness.mli b/infer/src/checkers/liveness.mli
index 0a4bb464e..0065d87b9 100644
--- a/infer/src/checkers/liveness.mli
+++ b/infer/src/checkers/liveness.mli
@@ -14,6 +14,6 @@ module PreAnalysisTransferFunctions (CFG : ProcCfg.S) :
   TransferFunctions.SIL
     with module CFG = CFG
      and module Domain = Domain
-     and type extras = ProcData.no_extras
+     and type analysis_data = unit ProcData.t
 
 val checker : Callbacks.proc_callback_args -> Summary.t
diff --git a/infer/src/checkers/preanal.ml b/infer/src/checkers/preanal.ml
index 2817113a2..e759c8895 100644
--- a/infer/src/checkers/preanal.ml
+++ b/infer/src/checkers/preanal.ml
@@ -161,7 +161,7 @@ module Liveness = struct
 
     module CFG = ProcCfg.Exceptional
 
-    type extras = LivenessAnalysis.invariant_map
+    type analysis_data = LivenessAnalysis.invariant_map ProcData.t
 
     let postprocess ((reaching_defs, _) as astate) node {ProcData.extras} =
       let node_id = Procdesc.Node.get_id (CFG.Node.underlying_node node) in
@@ -234,14 +234,18 @@ module Liveness = struct
         (* 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 summary tenv) ~initial with
+        match
+          AddressTaken.Analyzer.compute_post
+            {ProcData.summary; tenv; extras= ()}
+            ~initial (Summary.get_proc_desc summary)
+        with
         | Some post ->
             post
         | None ->
             AddressTaken.Domain.empty
     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 nullify_proc_data = {ProcData.summary; tenv; extras= 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 *)
@@ -298,7 +302,7 @@ module Liveness = struct
     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 summary tenv) ~initial
+      LivenessAnalysis.exec_cfg liveness_proc_cfg {ProcData.summary; tenv; extras= ()} ~initial
     in
     add_nullify_instrs summary tenv liveness_inv_map
 end
diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml
index 3a2d039ce..f51106a37 100644
--- a/infer/src/checkers/purity.ml
+++ b/infer/src/checkers/purity.ml
@@ -29,7 +29,7 @@ module TransferFunctions = struct
   module CFG = ProcCfg.Normal
   module Domain = PurityDomain
 
-  type extras = purity_extras
+  type analysis_data = purity_extras ProcData.t
 
   let get_alias_set inferbo_mem var =
     let default = ModifiedVarSet.empty in
@@ -215,12 +215,15 @@ let report_errors astate summary =
 
 let compute_summary summary tenv get_callee_summary inferbo_invariant_map =
   let proc_name = Summary.get_proc_name summary in
+  let proc_desc = Summary.get_proc_desc summary in
   let formals =
-    Procdesc.get_formals (Summary.get_proc_desc summary)
+    Procdesc.get_formals proc_desc
     |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name))
   in
-  let proc_data = ProcData.make summary tenv {inferbo_invariant_map; formals; get_callee_summary} in
-  Analyzer.compute_post proc_data ~initial:PurityDomain.pure
+  let proc_data =
+    {ProcData.summary; tenv; extras= {inferbo_invariant_map; formals; get_callee_summary}}
+  in
+  Analyzer.compute_post proc_data ~initial:PurityDomain.pure proc_desc
 
 
 let checker {Callbacks.exe_env; summary} : Summary.t =
diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml
index 59e209e1d..aae35d037 100644
--- a/infer/src/checkers/reachingDefs.ml
+++ b/infer/src/checkers/reachingDefs.ml
@@ -24,7 +24,7 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ReachingDefsMap
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   (* for each  x := e at node n, remove x's definitions and introduce x -> n *)
   let exec_instr astate _ (node : CFG.Node.t) instr =
@@ -70,7 +70,7 @@ type invariant_map = Analyzer.invariant_map
 
 let compute_invariant_map summary tenv =
   let pdesc = Summary.get_proc_desc summary in
-  let proc_data = ProcData.make_default summary tenv in
+  let proc_data = {ProcData.summary; tenv; extras= ()} 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/uninit.ml b/infer/src/checkers/uninit.ml
index d0c7798c8..42d86ccbb 100644
--- a/infer/src/checkers/uninit.ml
+++ b/infer/src/checkers/uninit.ml
@@ -75,7 +75,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = RecordDomain
 
-  type nonrec extras = extras
+  type analysis_data = extras ProcData.t
 
   let report_intra access_expr loc summary =
     let message =
@@ -352,9 +352,9 @@ let checker {Callbacks.exe_env; summary} : Summary.t =
   in
   let proc_data =
     let formals = FormalMap.make proc_desc in
-    ProcData.make summary tenv {formals; summary}
+    {ProcData.summary; tenv; extras= {formals; summary}}
   in
-  match Analyzer.compute_post proc_data ~initial with
+  match Analyzer.compute_post proc_data ~initial proc_desc with
   | Some {RecordDomain.prepost} ->
       Payload.update_summary prepost summary
   | None ->
diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml
index f67d500bd..e11b3bab1 100644
--- a/infer/src/concurrency/RacerD.ml
+++ b/infer/src/concurrency/RacerD.ml
@@ -23,7 +23,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = RacerDDomain
 
-  type extras = FormalMap.t
+  type analysis_data = FormalMap.t ProcData.t
 
   let rec get_access_exp = function
     | HilExp.AccessExpression access_expr ->
@@ -527,8 +527,8 @@ let analyze_procedure {Callbacks.exe_env; summary} =
     in
     let initial = set_initial_attributes tenv summary {bottom with ownership; threads; locks} in
     let formal_map = FormalMap.make proc_desc in
-    let proc_data = ProcData.make summary tenv formal_map in
-    Analyzer.compute_post proc_data ~initial
+    let proc_data = {ProcData.summary; tenv; extras= formal_map} in
+    Analyzer.compute_post proc_data ~initial proc_desc
     |> Option.map ~f:(astate_to_summary proc_desc formal_map)
     |> Option.value_map ~default:summary ~f:(fun post -> Payload.update_summary post summary)
   else Payload.update_summary empty_summary summary
diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml
index 0b45faada..35dade037 100644
--- a/infer/src/concurrency/starvation.ml
+++ b/infer/src/concurrency/starvation.ml
@@ -24,7 +24,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = FormalMap.t
+  type analysis_data = FormalMap.t ProcData.t
 
   let log_parse_error error pname actuals =
     L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Procname.pp pname
@@ -358,7 +358,7 @@ let analyze_procedure {Callbacks.exe_env; summary} =
   if StarvationModels.should_skip_analysis tenv procname [] then summary
   else
     let formals = FormalMap.make proc_desc in
-    let proc_data = ProcData.make summary tenv formals in
+    let proc_data = {ProcData.summary; tenv; extras= formals} in
     let loc = Procdesc.get_loc proc_desc in
     let set_lock_state_for_synchronized_proc astate =
       if Procdesc.is_java_synchronized proc_desc then
@@ -388,7 +388,7 @@ let analyze_procedure {Callbacks.exe_env; summary} =
       |> set_initial_attributes tenv summary
       |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation
     in
-    Analyzer.compute_post proc_data ~initial
+    Analyzer.compute_post proc_data ~initial proc_desc
     |> Option.map ~f:filter_blocks
     |> Option.map ~f:(Domain.summary_of_astate proc_desc)
     |> Option.fold ~init:summary ~f:(fun acc payload -> Payload.update_summary payload acc)
diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml
index 706f0c867..2fb3ae3f3 100644
--- a/infer/src/labs/ResourceLeaks.ml
+++ b/infer/src/labs/ResourceLeaks.ml
@@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ResourceLeakDomain
 
-  type extras = unit
+  type analysis_data = unit ProcData.t
 
   let is_closeable_typename tenv typename =
     let is_closable_interface typename _ =
@@ -88,8 +88,11 @@ let report_if_leak _post _summary (_proc_data : unit ProcData.t) = ()
 let checker {Callbacks.summary; exe_env} : Summary.t =
   let proc_name = Summary.get_proc_name summary in
   let tenv = Exe_env.get_tenv exe_env proc_name in
-  let proc_data = ProcData.make summary tenv () in
-  match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with
+  let proc_data = {ProcData.summary; tenv; extras= ()} in
+  match
+    Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial
+      (Summary.get_proc_desc summary)
+  with
   | Some post ->
       report_if_leak post summary proc_data ;
       Payload.update_summary post summary
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index a35bf7273..dfc5fd173 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -46,7 +46,7 @@ module PulseTransferFunctions = struct
   module CFG = ProcCfg.Normal
   module Domain = ExecutionDomain
 
-  type extras = get_formals
+  type analysis_data = get_formals ProcData.t
 
   let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate =
     match proc_name_of_call call_exp with
@@ -236,8 +236,8 @@ let checker {Callbacks.exe_env; summary} =
   let get_formals callee_pname =
     Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
   in
-  let proc_data = ProcData.make summary tenv get_formals in
-  match DisjunctiveAnalyzer.compute_post proc_data ~initial with
+  let proc_data = {ProcData.summary; tenv; extras= get_formals} in
+  match DisjunctiveAnalyzer.compute_post proc_data ~initial pdesc with
   | Some posts ->
       PulsePayload.update_summary (PulseSummary.of_posts pdesc posts) summary
   | None ->
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 10940f795..c4cca138e 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -28,7 +28,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     module CFG = CFG
     module Domain = Domain
 
-    type nonrec extras = extras
+    type analysis_data = extras ProcData.t
 
     (* get the node associated with [access_path] in [access_tree] *)
     let access_path_get_node access_path access_tree (proc_data : extras ProcData.t) =
@@ -863,8 +863,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       let formal_map = FormalMap.make proc_desc in
       {formal_map; summary}
     in
-    let proc_data = ProcData.make summary tenv extras in
-    match Analyzer.compute_post proc_data ~initial with
+    let proc_data = {ProcData.summary; tenv; extras} in
+    match Analyzer.compute_post proc_data ~initial proc_desc with
     | Some access_tree ->
         Payload.update_summary (make_summary proc_data access_tree) summary
     | None ->
diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml
index 87538aacb..bfb028042 100644
--- a/infer/src/unit/TaintTests.ml
+++ b/infer/src/unit/TaintTests.ml
@@ -153,7 +153,10 @@ let tests =
     ; ( "sink without source not tracked"
       , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ]
     |> TestInterpreter.create_tests ~pp_opt:pp_sparse
-         {formal_map= FormalMap.empty; summary= Summary.OnDisk.dummy}
+         (fun summary ->
+           { ProcData.summary
+           ; tenv= Tenv.create ()
+           ; extras= {formal_map= FormalMap.empty; summary= Summary.OnDisk.dummy} } )
          ~initial:(MockTaintAnalysis.Domain.bottom, Bindings.empty)
   in
   "taint_test_suite" >::: test_list
diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml
index 24132fa7b..b26216114 100644
--- a/infer/src/unit/abstractInterpreterTests.ml
+++ b/infer/src/unit/abstractInterpreterTests.ml
@@ -49,7 +49,7 @@ module PathCountTransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = PathCountDomain
 
-  type extras = ProcData.no_extras
+  type analysis_data = unit ProcData.t
 
   (* just propagate the current path count *)
   let exec_instr astate _ _ _ = astate
@@ -102,7 +102,9 @@ let tests =
             , (* we expect the finally block to be visited *)
               [invariant "1"] )
         ; invariant "1" ] ) ]
-    |> NormalTestInterpreter.create_tests ProcData.empty_extras ~initial
+    |> NormalTestInterpreter.create_tests
+         (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()})
+         ~initial
   in
   let exceptional_test_list =
     [ ( "try1"
@@ -127,6 +129,8 @@ let tests =
             , (* could arrive here via (1, 2, 3), (1, 4), or (2, 4) *)
               [invariant "3"] )
         ; invariant "3" ] ) ]
-    |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras ~initial
+    |> ExceptionalTestInterpreter.create_tests
+         (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()})
+         ~initial
   in
   "analyzer_tests_suite" >::: normal_test_list @ exceptional_test_list
diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml
index efbb05df5..79e282289 100644
--- a/infer/src/unit/addressTakenTests.ml
+++ b/infer/src/unit/addressTakenTests.ml
@@ -57,6 +57,8 @@ let tests =
         ; invariant "{ &b, &d }"
         ; var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f"
         ; invariant "{ &b, &f, &d }" ] ) ]
-    |> TestInterpreter.create_tests ProcData.empty_extras ~initial:AddressTaken.Domain.empty
+    |> TestInterpreter.create_tests
+         (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()})
+         ~initial:AddressTaken.Domain.empty
   in
   "address_taken_suite" >::: test_list
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 3ab84b715..110546aff 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -251,10 +251,12 @@ struct
     (Summary.OnDisk.reset pdesc, assert_map)
 
 
-  let create_test test_program extras ~initial pp_opt test_pname _ =
+  let create_test test_program make_analysis_data ~initial pp_opt test_pname _ =
     let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt 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 inv_map =
+      I.exec_pdesc (make_analysis_data summary) ~initial (Summary.get_proc_desc summary)
+    in
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =
         try
@@ -293,11 +295,12 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) =
 
   let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)]
 
-  let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt extras tests =
+  let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests =
     let open OUnit2 in
     List.concat_map
       ~f:(fun (name, test_program) ->
         List.map ai_list ~f:(fun (ai_name, create_test) ->
-            name ^ "_" ^ ai_name >:: create_test test_program extras ~initial pp_opt test_pname ) )
+            name ^ "_" ^ ai_name
+            >:: create_test test_program make_analysis_data ~initial pp_opt test_pname ) )
       tests
 end
diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml
index 120bab027..5162784da 100644
--- a/infer/src/unit/livenessTests.ml
+++ b/infer/src/unit/livenessTests.ml
@@ -97,6 +97,8 @@ let tests =
         ; While (unknown_cond, [id_assign_var "b" "d"])
         ; invariant "{ b }"
         ; id_assign_var "a" "b" ] ) ]
-    |> TestInterpreter.create_tests ProcData.empty_extras ~initial:Liveness.Domain.empty
+    |> TestInterpreter.create_tests
+         (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()})
+         ~initial:Liveness.Domain.empty
   in
   "liveness_test_suite" >::: test_list