Remove redundant fields from proc_callback_args

Summary:
The fields `tenv` and `integer_type_widths` can be obtained from the `exe_env` field of `proc_callback_args`

This commit removes the redundant fields

Reviewed By: ngorogiannis

Differential Revision: D16149520

fbshipit-source-id: d37526fd4

infer/src/backend/callbacks.ml

@@ -10,11 +10,7 @@ open! IStd
 (** Module to register and invoke callbacks *)
 
 type proc_callback_args =
-  { get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
-  ; tenv: Tenv.t
-  ; integer_type_widths: Typ.IntegerWidths.t
-  ; summary: Summary.t
-  ; exe_env: Exe_env.t }
+  {get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list; summary: Summary.t; exe_env: Exe_env.t}
 
 type proc_callback_t = proc_callback_args -> Summary.t
 
@@ -65,8 +61,6 @@ let iterate_procedure_callbacks exe_env summary =
     in
     Option.value_map source_file ~default:[] ~f:SourceFiles.proc_names_of_source
   in
-  let tenv = Exe_env.get_tenv exe_env proc_name in
-  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
   let is_specialized = Procdesc.is_specialized proc_desc in
   List.fold ~init:summary
     ~f:(fun summary {name; dynamic_dispatch; language; callback} ->
@@ -77,7 +71,7 @@ let iterate_procedure_callbacks exe_env summary =
               log_begin_event logger ~name ~categories:["backend"]
                 ~arguments:[("proc", `String (Typ.Procname.to_string proc_name))]
                 () )) ;
-        let summary = callback {get_procs_in_file; tenv; integer_type_widths; summary; exe_env} in
+        let summary = callback {get_procs_in_file; summary; exe_env} in
         PerfEvent.(log (fun logger -> log_end_event logger ())) ;
         summary )
       else summary )

infer/src/backend/callbacks.mli

@@ -10,11 +10,7 @@ open! IStd
 (** Module to register and invoke callbacks *)
 
 type proc_callback_args =
-  { get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
-  ; tenv: Tenv.t
-  ; integer_type_widths: Typ.IntegerWidths.t
-  ; summary: Summary.t
-  ; exe_env: Exe_env.t }
+  {get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list; summary: Summary.t; exe_env: Exe_env.t}
 
 (** Type of a procedure callback:
     - List of all the procedures the callback will be called on.

infer/src/biabduction/interproc.ml

@@ -1250,7 +1250,8 @@ let analyze_procedure_aux summary exe_env tenv : Summary.t =
   summary_compact
 
 
-let analyze_procedure {Callbacks.summary; tenv; exe_env} : Summary.t =
+let analyze_procedure {Callbacks.summary; exe_env} : Summary.t =
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
   if Topl.is_active () then Topl.instrument tenv (Summary.get_proc_desc summary) ;

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -372,8 +372,11 @@ let compute_summary :
 
 
 let do_analysis : Callbacks.proc_callback_args -> Summary.t =
- fun {tenv; integer_type_widths; summary} ->
+ fun {exe_env; summary} ->
   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 proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name 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

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -422,8 +422,11 @@ let get_checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_s
 
 
 let checker : Callbacks.proc_callback_args -> Summary.t =
- fun {tenv; integer_type_widths; summary} ->
+ fun {exe_env; summary} ->
   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 proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
   let inv_map =
     BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
   in

infer/src/checkers/Litho.ml

@@ -274,8 +274,9 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional))
 
-let checker {Callbacks.summary; tenv} =
+let checker {Callbacks.summary; exe_env} =
   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
   match Analyzer.compute_post proc_data ~initial:Domain.empty with
   | Some post ->

infer/src/checkers/SimpleChecker.ml

@@ -79,9 +79,10 @@ module Make (Spec : Spec) : S = struct
 
   module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
-  let checker {Callbacks.tenv; summary} : Summary.t =
+  let checker {Callbacks.exe_env; summary} : Summary.t =
     let proc_desc = Summary.get_proc_desc summary in
     let proc_name = Procdesc.get_proc_name proc_desc in
+    let tenv = Exe_env.get_tenv exe_env proc_name in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =
       let astate_set = state.AbstractInterpreter.State.post in

infer/src/checkers/Siof.ml

@@ -268,9 +268,10 @@ let siof_check gname (summary : Summary.t) =
       ()
 
 
-let checker {Callbacks.tenv; summary; get_procs_in_file} : Summary.t =
+let checker {Callbacks.exe_env; summary; get_procs_in_file} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let pname = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env pname in
   let standard_streams_initialized_in_tu =
     let includes_iostream tu =
       let magic_iostream_marker =

infer/src/checkers/annotationReachability.ml

@@ -214,9 +214,10 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si
     sink_map
 
 
-let report_src_snk_path {Callbacks.tenv; summary} sink_map snk_annot src_annot =
+let report_src_snk_path {Callbacks.exe_env; summary} sink_map snk_annot src_annot =
   let proc_desc = Summary.get_proc_desc summary in
   let proc_name = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
   let loc = Procdesc.get_loc proc_desc in
   if method_overrides_annot src_annot tenv proc_name then
     let f_report = report_annotation_stack src_annot.Annot.class_name snk_annot.Annot.class_name in
@@ -438,9 +439,10 @@ module ExpensiveAnnotationSpec = struct
 
   let method_is_expensive tenv pname = is_modeled_expensive tenv pname || is_expensive tenv pname
 
-  let check_expensive_subtyping_rules {Callbacks.tenv; summary} overridden_pname =
+  let check_expensive_subtyping_rules {Callbacks.exe_env; summary} overridden_pname =
     let proc_desc = Summary.get_proc_desc summary in
     let proc_name = Procdesc.get_proc_name proc_desc in
+    let tenv = Exe_env.get_tenv exe_env proc_name in
     let loc = Procdesc.get_loc proc_desc in
     if not (method_is_expensive tenv overridden_pname) then
       let description =
@@ -465,9 +467,10 @@ module ExpensiveAnnotationSpec = struct
     ; sanitizer_predicate= default_sanitizer
     ; sink_annotation= expensive_annot
     ; report=
-        (fun ({Callbacks.tenv; summary} as proc_data) astate ->
+        (fun ({Callbacks.exe_env; summary} as proc_data) astate ->
           let proc_desc = Summary.get_proc_desc summary in
           let proc_name = Procdesc.get_proc_name proc_desc in
+          let tenv = Exe_env.get_tenv exe_env proc_name in
           if is_expensive tenv proc_name then
             PatternMatch.override_iter (check_expensive_subtyping_rules proc_data) tenv proc_name ;
           report_src_snk_paths proc_data astate [performance_critical_annot] expensive_annot ) }
@@ -613,10 +616,11 @@ end
 
 module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
-let checker ({Callbacks.tenv; summary} as callback) : Summary.t =
-  let proc_desc = Summary.get_proc_desc summary in
+let checker ({Callbacks.exe_env; summary} as callback) : Summary.t =
+  let proc_name = Summary.get_proc_name summary in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
   let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in
-  let specs = get_annot_specs (Procdesc.get_proc_name proc_desc) 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
   | Some (annot_map, _) ->

infer/src/checkers/classLoads.ml

@@ -126,9 +126,10 @@ let report_loads summary astate =
            ClassLoadsDomain.iter report_load astate )
 
 
-let analyze_procedure {Callbacks.tenv; summary} =
+let analyze_procedure {Callbacks.exe_env; summary} =
   let proc_desc = Summary.get_proc_desc summary in
   let proc_name = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
   L.debug Analysis Verbose "CL: ANALYZING %a@." Typ.Procname.pp proc_name ;
   let loc = Procdesc.get_loc proc_desc in
   (* load the method's class *)

infer/src/checkers/cost.ml

@@ -792,7 +792,10 @@ let get_cost_summary astate = CostDomain.{post= astate.WorstCaseCost.costs}
 
 let report_errors proc_desc astate summary = Check.check_and_report astate proc_desc summary
 
-let checker {Callbacks.tenv; integer_type_widths; summary} : Summary.t =
+let checker {Callbacks.exe_env; summary} : Summary.t =
+  let proc_name = Summary.get_proc_name summary in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
   let proc_desc = Summary.get_proc_desc summary in
   let inferbo_invariant_map =
     BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
@@ -837,8 +840,7 @@ let checker {Callbacks.tenv; integer_type_widths; summary} : Summary.t =
   let () =
     let exit_cost_record = astate.WorstCaseCost.costs in
     L.(debug Analysis Verbose)
-      "@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Typ.Procname.pp
-      (Procdesc.get_proc_name proc_desc)
+      "@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Typ.Procname.pp proc_name
       (Container.length ~fold:NodeCFG.fold_nodes node_cfg)
       CostDomain.VariantCostMap.pp exit_cost_record
   in

infer/src/checkers/dataflow.ml

@@ -161,8 +161,9 @@ end
 (* MakeDF *)
 
 (** Example dataflow callback: compute the the distance from a node to the start node. *)
-let _callback_test_dataflow {Callbacks.tenv; summary} =
+let _callback_test_dataflow {Callbacks.exe_env; summary} =
   let proc_desc = Summary.get_proc_desc summary in
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let verbose = false in
   let module DFCount = MakeDF (struct
     type t = int

infer/src/checkers/fragmentRetainsViewChecker.ml

@@ -47,9 +47,10 @@ let report_warning class_name fld fld_typ summary =
   Reporting.log_warning summary ~loc IssueType.checkers_fragment_retain_view description
 
 
-let callback_fragment_retains_view_java java_pname {Callbacks.summary; tenv} =
+let callback_fragment_retains_view_java java_pname {Callbacks.summary; exe_env} =
   (* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *)
   (* TODO: handle fields nullified in callees in the same file *)
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let is_on_destroy_view =
     String.equal (Typ.Procname.Java.get_method java_pname) on_destroy_view
   in

infer/src/checkers/hoisting.ml

@@ -149,8 +149,11 @@ let report_errors proc_desc tenv get_callee_purity reaching_defs_invariant_map
     loop_head_to_inv_instrs
 
 
-let checker Callbacks.{tenv; summary; integer_type_widths} : Summary.t =
+let checker Callbacks.{summary; exe_env} : Summary.t =
   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 proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name 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 summary tenv in

infer/src/checkers/inefficientKeysetIterator.ml

@@ -97,8 +97,9 @@ let when_dominating_preds_satisfy idom my_node ~fun_name ~class_name_f ~f =
   aux my_node 4
 
 
-let checker Callbacks.{summary; tenv} : Summary.t =
+let checker Callbacks.{summary; exe_env} : 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 cfg = CFG.from_pdesc proc_desc in
   let _, loop_head_to_loop_nodes = Loop_control.get_loop_control_maps cfg in
   let idom = Dominators.get_idoms proc_desc in

infer/src/checkers/liveness.ml

@@ -211,8 +211,9 @@ let get_captured_by_ref_invariant_map proc_desc proc_data =
   CapturedByRefAnalyzer.exec_cfg cfg proc_data ~initial:VarSet.empty
 
 
-let checker {Callbacks.tenv; summary} : Summary.t =
+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 captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc proc_data in
   let cfg = CFG.from_pdesc proc_desc in

infer/src/checkers/printfArgs.ml

@@ -169,9 +169,10 @@ let check_printf_args_ok tenv (node : Procdesc.Node.t) (instr : Sil.instr)
       ()
 
 
-let callback_printf_args {Callbacks.tenv; summary} : Summary.t =
+let callback_printf_args {Callbacks.exe_env; summary} : Summary.t =
   let proc_desc = Summary.get_proc_desc summary in
   let proc_name = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
   Procdesc.iter_instrs
     (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc summary)
     proc_desc ;

infer/src/checkers/purity.ml

@@ -224,7 +224,10 @@ let compute_summary summary tenv get_callee_summary inferbo_invariant_map =
   Analyzer.compute_post proc_data ~initial:PurityDomain.pure
 
 
-let checker {Callbacks.tenv; summary; integer_type_widths} : Summary.t =
+let checker {Callbacks.exe_env; summary} : Summary.t =
+  let proc_name = Summary.get_proc_name summary in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
+  let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
   let inferbo_invariant_map =
     BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths
   in

infer/src/checkers/uninit.ml

@@ -338,8 +338,10 @@ module Initial = struct
             base_access_expr :: acc )
 end
 
-let checker {Callbacks.tenv; summary} : Summary.t =
+let checker {Callbacks.exe_env; summary} : Summary.t =
   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 proc_name in
   (* start with empty set of uninit local vars and empty set of init formal params *)
   let maybe_uninit_vars = Initial.get_locals tenv proc_desc in
   let initial =
@@ -356,7 +358,6 @@ let checker {Callbacks.tenv; summary} : Summary.t =
       Payload.update_summary prepost summary
   | None ->
       if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
-        L.internal_error "Uninit analyzer failed to compute post for %a" Typ.Procname.pp
-          (Procdesc.get_proc_name proc_desc) ;
+        L.internal_error "Uninit analyzer failed to compute post for %a" Typ.Procname.pp proc_name ;
         summary )
       else summary

infer/src/concurrency/RacerD.ml

@@ -507,8 +507,10 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal))
 
-let analyze_procedure {Callbacks.tenv; summary} =
+let analyze_procedure {Callbacks.exe_env; summary} =
   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 proc_name in
   let open RacerDModels in
   let open ConcurrencyModels in
   let method_annotation = (Procdesc.get_attributes proc_desc).method_annotation in
@@ -531,7 +533,7 @@ let analyze_procedure {Callbacks.tenv; summary} =
         else ThreadsDomain.NoThread
       in
       let add_owned_local acc (var_data : ProcAttributes.var_data) =
-        let pvar = Pvar.mk var_data.name (Procdesc.get_proc_name proc_desc) in
+        let pvar = Pvar.mk var_data.name proc_name in
         let base = AccessPath.base_of_pvar pvar var_data.typ in
         OwnershipDomain.add (base, []) OwnershipAbstractValue.owned acc
       in
@@ -553,7 +555,7 @@ let analyze_procedure {Callbacks.tenv; summary} =
         in
         OwnershipDomain.add (formal, []) ownership_value acc
       in
-      if is_initializer tenv (Procdesc.get_proc_name proc_desc) then
+      if is_initializer tenv proc_name then
         let add_owned_formal acc formal_index =
           match FormalMap.get_formal_base formal_index formal_map with
           | Some base ->
@@ -588,9 +590,7 @@ let analyze_procedure {Callbacks.tenv; summary} =
     match Analyzer.compute_post proc_data ~initial with
     | Some {threads; locks; accesses; ownership; attribute_map} ->
         let return_var_ap =
-          AccessPath.of_pvar
-            (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
-            (Procdesc.get_ret_type proc_desc)
+          AccessPath.of_pvar (Pvar.get_ret_pvar proc_name) (Procdesc.get_ret_type proc_desc)
         in
         let return_ownership = OwnershipDomain.get_owned return_var_ap ownership in
         let return_attributes =

infer/src/concurrency/starvation.ml

@@ -134,10 +134,11 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal))
 
-let analyze_procedure {Callbacks.tenv; summary} =
+let analyze_procedure {Callbacks.exe_env; summary} =
   let proc_desc = Summary.get_proc_desc summary in
   let open StarvationDomain in
   let pname = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env pname in
   if StarvationModels.should_skip_analysis tenv pname [] then summary
   else
     let formals = FormalMap.make proc_desc in

infer/src/labs/ResourceLeaks.ml

@@ -86,13 +86,13 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (CFG))
 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 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
   | Some post ->
       report_if_leak post summary proc_data ;
       Payload.update_summary post summary
   | None ->
-      L.(die InternalError)
-        "Analyzer failed to compute post for %a" Typ.Procname.pp
-        (Summary.get_proc_name proc_data.summary)
+      L.(die InternalError) "Analyzer failed to compute post for %a" Typ.Procname.pp proc_name

infer/src/nullsafe/NullabilityCheck.ml

@@ -336,8 +336,9 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Exceptional))
 
-let checker {Callbacks.summary; tenv} =
+let checker {Callbacks.summary; exe_env} =
   let initial = (NullableAP.empty, NullCheckedPname.empty) in
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let proc_data = ProcData.make summary tenv () in
   ignore (Analyzer.compute_post proc_data ~initial) ;
   summary

infer/src/nullsafe/NullabilitySuggest.ml

@@ -179,9 +179,10 @@ let is_outside_codebase proc_name field_name =
       false
 
 
-let checker {Callbacks.summary; tenv} =
+let checker {Callbacks.summary; exe_env} =
   let proc_desc = Summary.get_proc_desc summary in
   let proc_name = Procdesc.get_proc_name proc_desc in
+  let tenv = Exe_env.get_tenv exe_env proc_name in
   let annotation = Localise.nullable_annotation_name proc_name in
   let report astate (proc_data : extras ProcData.t) =
     let report_access_path ap udchain =
@@ -211,7 +212,6 @@ let checker {Callbacks.summary; tenv} =
     in
     Domain.iter report_access_path astate
   in
-  let proc_name = Procdesc.get_proc_name proc_desc in
   if AndroidFramework.is_destroy_method proc_name then
     (* Skip the fields nullified in Fragment onDestroy and onDestroyView *)
     summary

infer/src/nullsafe/eradicate.ml

@@ -112,11 +112,12 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
         (!calls_this, None)
 
 
-  let callback2 calls_this checks {Callbacks.summary; tenv; get_procs_in_file} annotated_signature
-      linereader proc_loc : unit =
+  let callback2 calls_this checks {Callbacks.summary; exe_env; get_procs_in_file}
+      annotated_signature linereader proc_loc : unit =
     let curr_pdesc = Summary.get_proc_desc summary in
     let idenv = Idenv.create curr_pdesc in
     let curr_pname = Summary.get_proc_name summary in
+    let tenv = Exe_env.get_tenv exe_env curr_pname in
     let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
     let find_canonical_duplicate node =
       let duplicate_nodes = find_duplicate_nodes node in

infer/src/nullsafe/immutableChecker.ml

@@ -42,5 +42,6 @@ let check_immutable_cast tenv curr_pname curr_pdesc typ_expected typ_found_opt l
       ()
 
 
-let callback_check_immutable_cast ({Callbacks.tenv} as args) =
+let callback_check_immutable_cast ({Callbacks.exe_env; summary} as args) =
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   Eradicate.callback_check_return_type (check_immutable_cast tenv) args

infer/src/pulse/Pulse.ml

@@ -214,7 +214,8 @@ module DisjunctiveTransferFunctions =
 
 module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFunctions)
 
-let checker {Callbacks.tenv; summary} =
+let checker {Callbacks.exe_env; summary} =
+  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let proc_data = ProcData.make summary tenv () in
   AbstractAddress.init () ;
   let initial =

infer/src/quandary/TaintAnalysis.ml

@@ -846,11 +846,12 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     TaintSpecification.to_summary_access_tree with_footprint_vars
 
 
-  let checker {Callbacks.tenv; summary} : Summary.t =
+  let checker {Callbacks.exe_env; summary} : Summary.t =
     let proc_desc = Summary.get_proc_desc summary in
+    let pname = Procdesc.get_proc_name proc_desc in
+    let tenv = Exe_env.get_tenv exe_env pname in
     (* bind parameters to a trace with a tainted source (if applicable) *)
     let make_initial pdesc =
-      let pname = Procdesc.get_proc_name pdesc in
       List.fold
         ~f:(fun acc (name, typ, taint_opt) ->
           match taint_opt with
@@ -876,7 +877,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     | None ->
         if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
           L.internal_error "Couldn't compute post for %a. Broken CFG suspected" Typ.Procname.pp
-            (Procdesc.get_proc_name proc_desc) ;
+            pname ;
           summary )
         else summary
 end