diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml
index 7c0280c64..abca4c4c5 100644
--- a/infer/src/backend/callbacks.ml
+++ b/infer/src/backend/callbacks.ml
@@ -45,32 +45,33 @@ let unregister_all_callbacks () =
 
 (** Collect what we need to know about a procedure for the analysis. *)
 let get_procedure_definition exe_env proc_name =
-  let cfg = Exe_env.get_cfg exe_env proc_name in
   let tenv = Exe_env.get_tenv exe_env proc_name in
   Option.map
     (fun proc_desc ->
-       let idenv = Idenv.create cfg proc_desc
+       let idenv = Idenv.create proc_desc
        and language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
        (idenv, tenv, proc_name, proc_desc, language))
-    (Cfg.Procdesc.find_from_name cfg proc_name)
+    (Exe_env.get_proc_desc exe_env proc_name)
 
 let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP
 
-(** Invoke all registered procedure callbacks on a set of procedures. *)
-let iterate_procedure_callbacks exe_env proc_name =
-  let procedure_language = get_language proc_name in
+(** Invoke all registered procedure callbacks on the given procedure. *)
+let iterate_procedure_callbacks exe_env caller_pname =
+  let procedure_language = get_language caller_pname in
   Config.curr_language := procedure_language;
 
-  let cfg = Exe_env.get_cfg exe_env proc_name in
-  let get_cfg pname =
-    Some (Exe_env.get_cfg exe_env pname) in
+  let get_cfg proc_name =
+    Exe_env.get_cfg exe_env proc_name in
+
   let get_proc_desc proc_name =
-    let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in
-    Cfg.Procdesc.find_from_name cfg proc_name in
-  let get_procs_in_file proc_name =
-    let cfg = try Exe_env.get_cfg exe_env proc_name with Not_found -> cfg in
-    IList.map Cfg.Procdesc.get_proc_name (Cfg.get_defined_procs cfg) in
+    Exe_env.get_proc_desc exe_env proc_name in
 
+  let get_procs_in_file proc_name =
+    match Exe_env.get_cfg exe_env proc_name with
+    | Some cfg->
+        IList.map Cfg.Procdesc.get_proc_name (Cfg.get_defined_procs cfg)
+    | None ->
+        [] in
 
   let update_time proc_name elapsed =
     match Specs.get_summary proc_name with
@@ -105,15 +106,11 @@ let iterate_procedure_callbacks exe_env proc_name =
                 update_time proc_name elapsed
               end)
          !procedure_callbacks)
-    (get_procedure_definition exe_env proc_name)
+    (get_procedure_definition exe_env caller_pname)
 
 (** Invoke all registered cluster callbacks on a cluster of procedures. *)
 let iterate_cluster_callbacks all_procs exe_env proc_names =
-  let get_procdesc proc_name =
-    try
-      let cfg = Exe_env.get_cfg exe_env proc_name in
-      Cfg.Procdesc.find_from_name cfg proc_name
-    with Not_found -> None in
+  let get_procdesc = Exe_env.get_proc_desc exe_env in
 
   let procedure_definitions =
     IList.map (get_procedure_definition exe_env) proc_names
diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml
index 9976735cd..c9bbe83bf 100644
--- a/infer/src/backend/exe_env.ml
+++ b/infer/src/backend/exe_env.ml
@@ -123,35 +123,37 @@ let get_source exe_env pname =
   (get_file_data exe_env pname).source
 
 let file_data_to_tenv file_data =
-  if file_data.tenv == None then file_data.tenv <- Sil.load_tenv_from_file file_data.tenv_file;
-  match file_data.tenv with
-  | None ->
-      L.err "Cannot find tenv for %s@." (DB.filename_to_string file_data.tenv_file);
-      assert false
-  | Some tenv -> tenv
+  if file_data.tenv == None
+  then file_data.tenv <- Sil.load_tenv_from_file file_data.tenv_file;
+  file_data.tenv
 
 let file_data_to_cfg file_data =
-  match file_data.cfg with
-  | None ->
-      let cfg = match Cfg.load_cfg_from_file file_data.cfg_file with
-        | None ->
-            L.err "Cannot find cfg for %s@." (DB.filename_to_string file_data.cfg_file);
-            assert false
-        | Some cfg -> cfg in
-      file_data.cfg <- Some cfg;
-      cfg
-  | Some cfg -> cfg
+  if file_data.cfg = None
+  then file_data.cfg <- Cfg.load_cfg_from_file file_data.cfg_file;
+  file_data.cfg
 
 (** return the type environment associated to the procedure *)
-let get_tenv exe_env pname =
-  let file_data = get_file_data exe_env pname in
-  file_data_to_tenv file_data
+let get_tenv exe_env proc_name : Sil.tenv =
+  let file_data = get_file_data exe_env proc_name in
+  match file_data_to_tenv file_data with
+  | Some tenv ->
+      tenv
+  | None ->
+      failwith ("get_tenv: tenv not found for" ^ Procname.to_string proc_name)
 
 (** return the cfg associated to the procedure *)
 let get_cfg exe_env pname =
   let file_data = get_file_data exe_env pname in
   file_data_to_cfg file_data
 
+(** return the proc desc associated to the procedure *)
+let get_proc_desc exe_env pname =
+  match get_cfg exe_env pname with
+  | Some cfg ->
+      Cfg.Procdesc.find_from_name cfg pname
+  | None ->
+      None
+
 (** [iter_files f exe_env] applies [f] to the filename and tenv and cfg for each file in [exe_env] *)
 let iter_files f exe_env =
   let do_file _ file_data seen_files_acc =
@@ -164,26 +166,7 @@ let iter_files f exe_env =
       begin
         DB.current_source := fname;
         Config.nLOC := file_data.nLOC;
-        f fname (file_data_to_cfg file_data);
+        Option.may (fun cfg -> f fname cfg) (file_data_to_cfg file_data);
         DB.SourceFileSet.add fname seen_files_acc
       end in
   ignore (Procname.Hash.fold do_file exe_env.proc_map DB.SourceFileSet.empty)
-
-(*
-(** return the procs enabled: active and not shadowed, plus the procs they call directly *)
-let procs_enabled exe_env source =
-  let is_not_shadowed proc_name = (* not shadowed by a definition in another file *)
-    DB.source_file_equal (get_source exe_env proc_name) source in
-  match exe_env.active_opt with
-  | Some pset ->
-      let res = ref Procname.Set.empty in
-      (* add any proc which is not shadowed, and all the procs it calls *)
-      let do_pname proc_name =
-        if is_not_shadowed proc_name then
-          let pset' = Cg.get_all_children exe_env.cg proc_name in
-          let pset'' = Procname.Set.add proc_name pset' in
-          res := Procname.Set.union pset'' !res in
-      Procname.Set.iter do_pname pset;
-      Some !res
-  | None -> None
-*)
diff --git a/infer/src/backend/exe_env.mli b/infer/src/backend/exe_env.mli
index 3e710aa21..29099f4d0 100644
--- a/infer/src/backend/exe_env.mli
+++ b/infer/src/backend/exe_env.mli
@@ -36,7 +36,10 @@ val get_source : t -> Procname.t -> DB.source_file
 val get_tenv : t -> Procname.t -> Sil.tenv
 
 (** return the cfg associated to the procedure *)
-val get_cfg : t -> Procname.t -> Cfg.cfg
+val get_cfg : t -> Procname.t -> Cfg.cfg option
+
+(** return the proc desc associated to the procedure *)
+val get_proc_desc : t -> Procname.t -> Cfg.Procdesc.t option
 
 (** [iter_files f exe_env] applies [f] to the source file and tenv and cfg for each file in [exe_env] *)
 val iter_files : (DB.source_file -> Cfg.cfg -> unit) -> t -> unit
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index c3ca5beb1..fe358b928 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -194,7 +194,7 @@ let do_meet_pre pset =
     Propset.to_proplist pset
 
 (** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *)
-let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list =
+let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
   let collect_do_abstract_one tenv prop =
     if !Config.footprint
     then
@@ -203,7 +203,10 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
         prop
     else
       Abs.abstract_no_symop tenv prop in
-  let pres = IList.map (fun spec -> Specs.Jprop.to_prop spec.Specs.pre) (Specs.get_specs proc_name) in
+  let pres =
+    IList.map
+      (fun spec -> Specs.Jprop.to_prop spec.Specs.pre)
+      (Specs.get_specs proc_name) in
   let pset = Propset.from_proplist pres in
   let pset' =
     let f p = Prop.prop_normal_vars_to_primed_vars p in
@@ -212,10 +215,11 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
   L.d_strln ("#### Extracted footprint of " ^ Procname.to_string proc_name ^ ":  ####");
   L.d_increase_indent 1; Propset.d Prop.prop_emp pset'; L.d_decrease_indent 1; L.d_ln ();
   L.d_ln ();
-  let pset'' = collect_do_abstract_pre pname tenv pset' in
+  let pset'' = collect_do_abstract_pre proc_name tenv pset' in
   let plist_meet = do_meet_pre pset'' in
   L.d_strln ("#### Footprint of " ^ Procname.to_string proc_name ^ " after Meet  ####");
-  L.d_increase_indent 1; Propgraph.d_proplist Prop.prop_emp plist_meet; L.d_decrease_indent 1; L.d_ln ();
+  L.d_increase_indent 1; Propgraph.d_proplist Prop.prop_emp plist_meet;
+  L.d_decrease_indent 1; L.d_ln ();
   L.d_ln ();
   L.d_increase_indent 2; (* Indent for the join output *)
   let jplist = do_join_pre plist_meet in
@@ -226,7 +230,9 @@ let collect_preconditions pname tenv proc_name : Prop.normal Specs.Jprop.t list
   L.d_strln ("#### Renamed footprint of " ^ Procname.to_string proc_name ^ ":  ####");
   L.d_increase_indent 1; Specs.Jprop.d_list false jplist'; L.d_decrease_indent 1; L.d_ln ();
   let jplist'' =
-    let f p = Prop.prop_primed_vars_to_normal_vars (collect_do_abstract_one pname tenv p) in
+    let f p =
+      Prop.prop_primed_vars_to_normal_vars
+        (collect_do_abstract_one proc_name tenv p) in
     IList.map (Specs.Jprop.map f) jplist' in
   L.d_strln ("#### Abstracted footprint of " ^ Procname.to_string proc_name ^ ":  ####");
   L.d_increase_indent 1; Specs.Jprop.d_list false jplist''; L.d_decrease_indent 1; L.d_ln();
@@ -1217,14 +1223,13 @@ let transition_footprint_re_exe proc_name joined_pres =
 
 (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
     the procedures enabled after the analysis of [proc_name] *)
-let perform_transition exe_env proc_name =
-  let transition pname =
-    let tenv = Exe_env.get_tenv exe_env pname in
+let perform_transition exe_env tenv proc_name =
+  let transition () =
     let joined_pres = (* disable exceptions for leaks and protect against any other errors *)
       let allowleak = !Config.allowleak in
       let apply_start_node f = (* apply the start node to f, and do nothing in case of exception *)
         try
-          match Cfg.Procdesc.find_from_name (Exe_env.get_cfg exe_env pname) pname with
+          match Exe_env.get_proc_desc exe_env proc_name with
           | Some pdesc ->
               let start_node = Cfg.Procdesc.get_start_node pdesc in
               f start_node
@@ -1233,7 +1238,7 @@ let perform_transition exe_env proc_name =
       apply_start_node (do_before_node 0);
       try
         Config.allowleak := true;
-        let res = collect_preconditions proc_name tenv pname in
+        let res = collect_preconditions tenv proc_name in
         Config.allowleak := allowleak;
         apply_start_node do_after_node;
         res
@@ -1245,9 +1250,9 @@ let perform_transition exe_env proc_name =
         let err_str = "exception raised " ^ (Localise.to_string err_name) in
         L.err "Error: %s %a@." err_str pp_ml_loc_opt ml_loc_opt;
         [] in
-    transition_footprint_re_exe pname joined_pres in
+    transition_footprint_re_exe proc_name joined_pres in
   if Specs.get_phase proc_name == Specs.FOOTPRINT
-  then transition proc_name
+  then transition ()
 
 
 let interprocedural_algorithm exe_env : unit =
@@ -1258,25 +1263,21 @@ let interprocedural_algorithm exe_env : unit =
   let procs_to_analyze =
     IList.filter filter_initial (Cg.get_defined_nodes call_graph) in
   let to_analyze proc_name =
-    try
-      let cfg = Exe_env.get_cfg exe_env proc_name in
-      match Cfg.Procdesc.find_from_name cfg proc_name with
-      | Some pdesc ->
-          let reactive_changed =
-            if !Config.reactive_mode
-            then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed
-            else true in
-          if
-            reactive_changed && (* in reactive mode, only analyze changed procedures *)
-            Ondemand.procedure_should_be_analyzed proc_name
-          then
-            Some pdesc
-          else
-            None
-      | None ->
+    match Exe_env.get_proc_desc exe_env proc_name with
+    | Some proc_desc ->
+        let reactive_changed =
+          if !Config.reactive_mode
+          then (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.changed
+          else true in
+        if
+          reactive_changed && (* in reactive mode, only analyze changed procedures *)
+          Ondemand.procedure_should_be_analyzed proc_name
+        then
+          Some proc_desc
+        else
           None
-    with Not_found ->
-      None in
+    | None ->
+        None in
   let process_one_proc proc_name =
     match to_analyze proc_name with
     | Some pdesc ->
@@ -1295,10 +1296,11 @@ let do_analysis exe_env =
     Cfg.Procdesc.iter_calls f caller_pdesc;
     IList.rev !calls in
   let init_proc (pname, dep) =
-    let cfg = Exe_env.get_cfg exe_env pname in
-    let pdesc = match Cfg.Procdesc.find_from_name cfg pname with
-      | Some pdesc -> pdesc
-      | None -> assert false in
+    let pdesc = match Exe_env.get_proc_desc exe_env pname with
+      | Some pdesc ->
+          pdesc
+      | None ->
+          assert false in
     let nodes = IList.map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes pdesc) in
     let proc_flags = Cfg.Procdesc.get_flags pdesc in
     let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *)
@@ -1319,17 +1321,17 @@ let do_analysis exe_env =
 
   let callbacks =
     let get_cfg proc_name =
-      Some (Exe_env.get_cfg exe_env proc_name) in
+      Exe_env.get_cfg exe_env proc_name in
     let get_proc_desc proc_name =
-      let callee_cfg = Exe_env.get_cfg exe_env proc_name in
-      Cfg.Procdesc.find_from_name callee_cfg proc_name in
+      Exe_env.get_proc_desc exe_env proc_name in
     let analyze_ondemand proc_desc =
       let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
+      let tenv = Exe_env.get_tenv exe_env proc_name in
       let summaryfp =
         run_in_footprint_mode (analyze_proc exe_env) proc_desc in
       Specs.add_summary proc_name summaryfp;
 
-      perform_transition exe_env proc_name;
+      perform_transition exe_env tenv proc_name;
 
       let summaryre =
         run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
diff --git a/infer/src/checkers/idenv.ml b/infer/src/checkers/idenv.ml
index bde322e05..2ad5de673 100644
--- a/infer/src/checkers/idenv.ml
+++ b/infer/src/checkers/idenv.ml
@@ -11,9 +11,9 @@
     Lazy implementation: only created when actually used. *)
 
 
-type t = (Sil.exp Ident.IdentHash.t) Lazy.t * Cfg.cfg
+type t = (Sil.exp Ident.IdentHash.t) Lazy.t
 
-let _create proc_desc =
+let create_ proc_desc =
   let map = Ident.IdentHash.create 1 in
   let do_instr _ = function
     | Sil.Letderef (id, e, _, _) ->
@@ -23,17 +23,17 @@ let _create proc_desc =
   map
 
 (* lazy implementation, only create when used *)
-let create cfg proc_desc =
-  let map = lazy (_create proc_desc) in
-  map, cfg
+let create proc_desc =
+  let map = lazy (create_ proc_desc) in
+  map
 
 (* create an idenv for another procedure *)
-let create_from_idenv (_, cfg) proc_desc =
-  let map = lazy (_create proc_desc) in
-  map, cfg
+let create_from_idenv _ proc_desc =
+  let map = lazy (create_ proc_desc) in
+  map
 
-let lookup (_map, _) id =
-  let map = Lazy.force _map in
+let lookup map_ id =
+  let map = Lazy.force map_ in
   try
     Some (Ident.IdentHash.find map id)
   with Not_found -> None
diff --git a/infer/src/checkers/idenv.mli b/infer/src/checkers/idenv.mli
index 5a9a6978a..5e48646ba 100644
--- a/infer/src/checkers/idenv.mli
+++ b/infer/src/checkers/idenv.mli
@@ -13,7 +13,7 @@
 
 type t
 
-val create : Cfg.cfg -> Cfg.Procdesc.t -> t
+val create : Cfg.Procdesc.t -> t
 val create_from_idenv : t -> Cfg.Procdesc.t -> t
 val lookup : t -> Ident.t -> Sil.exp option
 val expand_expr : t -> Sil.exp -> Sil.exp