diff --git a/infer/src/absint/AnalysisCallbacks.ml b/infer/src/absint/AnalysisCallbacks.ml
index bc232fb2e..9ab8f00bb 100644
--- a/infer/src/absint/AnalysisCallbacks.ml
+++ b/infer/src/absint/AnalysisCallbacks.ml
@@ -9,11 +9,10 @@ open! IStd
 module L = Logging
 
 type callbacks =
-  { get_proc_desc_f: Procname.t -> Procdesc.t option
-  ; html_debug_new_node_session_f:
+  { html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
-  ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }
+  ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
 
 let callbacks_ref : callbacks option ref = ref None
 
@@ -27,10 +26,8 @@ let get_callbacks () =
       L.die InternalError "Callbacks not set"
 
 
-let get_proc_desc proc_name = (get_callbacks ()).get_proc_desc_f proc_name
-
 let html_debug_new_node_session ?kind ~pp_name node ~f =
   (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f
 
 
-let proc_resolve_attributes proc_name = (get_callbacks ()).proc_resolve_attributes_f proc_name
+let get_model_proc_desc proc_name = (get_callbacks ()).get_model_proc_desc_f proc_name
diff --git a/infer/src/absint/AnalysisCallbacks.mli b/infer/src/absint/AnalysisCallbacks.mli
index 3ceb31266..d6a388fdc 100644
--- a/infer/src/absint/AnalysisCallbacks.mli
+++ b/infer/src/absint/AnalysisCallbacks.mli
@@ -9,8 +9,8 @@ open! IStd
 
 (** {2 Analysis API} *)
 
-val get_proc_desc : Procname.t -> Procdesc.t option
-(** set to [Ondemand.get_proc_desc] *)
+val get_model_proc_desc : Procname.t -> Procdesc.t option
+(** get the preanalysed procdesc of a model; raises if procname given is not a biabduction model *)
 
 val html_debug_new_node_session :
      ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
@@ -20,20 +20,16 @@ val html_debug_new_node_session :
   -> 'a
 (** set to [NodePrinter.with_session] *)
 
-val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
-(** set to [Summary.OnDisk.proc_resolve_attributes] *)
-
 (** {2 Callbacks management}*)
 
 (** These callbacks are used to break the dependency cycles between some modules. Specifically, we
     put here functions needed for the analysis that depend on modules higher up the dependency graph
     than this library but whose type does not. *)
 type callbacks =
-  { get_proc_desc_f: Procname.t -> Procdesc.t option
-  ; html_debug_new_node_session_f:
+  { html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
-  ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }
+  ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
 
 val set_callbacks : callbacks -> unit
 (** make sure this is called before starting any actual analysis *)
diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml
index b95b45013..59ecea2d8 100644
--- a/infer/src/backend/CallbackOfChecker.ml
+++ b/infer/src/backend/CallbackOfChecker.ml
@@ -11,9 +11,8 @@ open! IStd
    crash) *)
 let () =
   AnalysisCallbacks.set_callbacks
-    { get_proc_desc_f= Ondemand.get_proc_desc
-    ; html_debug_new_node_session_f= NodePrinter.with_session
-    ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes }
+    { html_debug_new_node_session_f= NodePrinter.with_session
+    ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc }
 
 
 let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary
diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml
index 8d9c5535f..895a5706d 100644
--- a/infer/src/backend/Summary.ml
+++ b/infer/src/backend/Summary.ml
@@ -261,6 +261,13 @@ module OnDisk = struct
         load_summary_to_spec_table proc_name
 
 
+  let get_model_proc_desc model_name =
+    if not (BiabductionModels.mem model_name) then
+      Logging.die InternalError "Requested summary of model that couldn't be found: %a@\n"
+        Procname.pp model_name
+    else Option.map (get model_name) ~f:(fun (s : full_summary) -> s.proc_desc)
+
+
   (** Try to find the attributes for a defined proc. First look at specs (to get attributes computed
       by analysis) then look at the attributes table. If no attributes can be found, return None. *)
   let proc_resolve_attributes proc_name =
diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli
index 69db5d3f8..df04fc22a 100644
--- a/infer/src/backend/Summary.mli
+++ b/infer/src/backend/Summary.mli
@@ -99,4 +99,6 @@ module OnDisk : sig
 
   val pp_specs_from_config : Format.formatter -> unit
   (** pretty print all stored summaries *)
+
+  val get_model_proc_desc : Procname.t -> Procdesc.t option
 end
diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli
index b7933f214..63b6fd430 100644
--- a/infer/src/backend/ondemand.mli
+++ b/infer/src/backend/ondemand.mli
@@ -9,9 +9,6 @@ open! IStd
 
 (** Module for on-demand analysis. *)
 
-val get_proc_desc : Procname.t -> Procdesc.t option
-(** Find a proc desc for the procedure, perhaps loading it from disk. *)
-
 val analyze_proc_name : Exe_env.t -> caller_summary:Summary.t -> Procname.t -> Summary.t option
 (** [analyze_proc_name exe_env ~caller_summary callee_pname] performs an on-demand analysis of
     [callee_pname] triggered during the analysis of [caller_summary] *)
diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index aac955d5d..73c312c39 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -590,6 +590,17 @@ type resolve_and_analyze_result =
   ; resolved_procdesc_opt: Procdesc.t option
   ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option }
 
+let get_proc_desc proc_name =
+  if BiabductionModels.mem proc_name then AnalysisCallbacks.get_model_proc_desc proc_name
+  else Procdesc.load proc_name
+
+
+let get_attributes proc_name =
+  if BiabductionModels.mem proc_name then
+    AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes
+  else Attributes.load proc_name
+
+
 (** Resolve the procedure name and run the analysis of the resolved procedure if not already
     analyzed *)
 let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv}
@@ -601,15 +612,15 @@ let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc;
        whether the method is defined or generated by the specialization *)
     let analyze_ondemand resolved_pname =
       if Procname.equal resolved_pname callee_proc_name then
-        (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name)
+        (get_proc_desc callee_proc_name, analyze_dependency callee_proc_name)
       else
         (* Create the type specialized procedure description and analyze it directly *)
         let resolved_proc_desc_option =
-          match AnalysisCallbacks.get_proc_desc resolved_pname with
+          match get_proc_desc resolved_pname with
           | Some _ as resolved_proc_desc ->
               resolved_proc_desc
           | None ->
-              let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in
+              let procdesc_opt = get_proc_desc callee_proc_name in
               Option.map procdesc_opt ~f:(fun callee_proc_desc ->
                   (* It is possible that the types of the arguments are not as precise as the type of
                      the objects in the heap, so we should update them to get the best results. *)
@@ -988,7 +999,7 @@ let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv;
 
 
 let is_variadic_procname callee_pname =
-  Option.exists (AnalysisCallbacks.proc_resolve_attributes callee_pname) ~f:(fun proc_attrs ->
+  Option.exists (get_attributes callee_pname) ~f:(fun proc_attrs ->
       proc_attrs.ProcAttributes.is_variadic )
 
 
@@ -1002,9 +1013,7 @@ let resolve_and_analyze_no_dynamic_dispatch {InterproceduralAnalysis.analyze_dep
         callee_pname
   in
   let resolved_summary_opt = analyze_dependency resolved_pname in
-  { resolved_pname
-  ; resolved_procdesc_opt= AnalysisCallbacks.get_proc_desc resolved_pname
-  ; resolved_summary_opt }
+  {resolved_pname; resolved_procdesc_opt= get_proc_desc resolved_pname; resolved_summary_opt}
 
 
 let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname call_flags =
@@ -1556,9 +1565,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
         callee_pname ret_annots loc path_pos
     in
     let callee_loc_opt =
-      Option.map
-        ~f:(fun attributes -> attributes.ProcAttributes.loc)
-        (AnalysisCallbacks.proc_resolve_attributes callee_pname)
+      Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (get_attributes callee_pname)
     in
     let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in
     [(prop_with_undef_attr, skip_path)]
@@ -1600,7 +1607,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po
 
 
 and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as builtin_args) =
-  match AnalysisCallbacks.proc_resolve_attributes proc_name with
+  match get_attributes proc_name with
   | Some callee_attributes -> (
     match callee_attributes.ProcAttributes.sentinel_attr with
     | Some sentinel ->
diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml
index 307da3918..c880f2289 100644
--- a/infer/src/biabduction/Tabulation.ml
+++ b/infer/src/biabduction/Tabulation.ml
@@ -745,9 +745,15 @@ let prop_set_exn tenv pname prop se_exn =
   Prop.normalize tenv (Prop.set prop ~sigma:sigma')
 
 
+let get_attributes proc_name =
+  if BiabductionModels.mem proc_name then
+    AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes
+  else Attributes.load proc_name
+
+
 (** Include a subtrace for a procedure call if the callee is not a model. *)
 let include_subtrace callee_pname =
-  match AnalysisCallbacks.proc_resolve_attributes callee_pname with
+  match get_attributes callee_pname with
   | Some attrs ->
       (not attrs.ProcAttributes.is_biabduction_model)
       && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 57fbacd1f..e56f598bf 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -300,9 +300,8 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) =
 
   let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests =
     AnalysisCallbacks.set_callbacks
-      { get_proc_desc_f= Ondemand.get_proc_desc
-      ; html_debug_new_node_session_f= NodePrinter.with_session
-      ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } ;
+      { html_debug_new_node_session_f= NodePrinter.with_session
+      ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } ;
     let open OUnit2 in
     List.concat_map
       ~f:(fun (name, test_program) ->