diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index 5b7dd39ac593226a1f5c91cdaa50908cd8881c7b..4d0628fa65ca5d099f85b41e83a47980ebcb31e9 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -232,7 +232,7 @@ and setup_precondition_proxy called_kf precondition =
     Kernel.debug "Setting up syntactic call-preconditions for precondition \
                   of %a" Kernel_function.pretty called_kf;
     let call_preconditions =
-      List.map
+      List.rev_map
         (fun (_,stmt) -> precondition_at_call called_kf precondition stmt)
         (Kernel_function.find_syntactic_callsites called_kf)
     in
diff --git a/src/plugins/callgraph/uses.ml b/src/plugins/callgraph/uses.ml
index c97873852eeb1cda09fc083e12a53d7a8869de18..3d50cf67113a40bbadd5f75060cd140ae3ae698d 100644
--- a/src/plugins/callgraph/uses.ml
+++ b/src/plugins/callgraph/uses.ml
@@ -101,38 +101,6 @@ let iter_on_aux iter_dir f kf =
 let iter_on_callers = iter_on_aux Cg.G.iter_pred
 let iter_on_callees = iter_on_aux Cg.G.iter_succ
 
-let is_local_or_formal_of_caller v kf =
-  try
-    iter_on_callers
-      (fun caller ->
-         if Base.is_formal_or_local v (Kernel_function.get_definition caller)
-         then raise Exit)
-      kf;
-    false
-  with Exit ->
-    true
-
-let accept_base ~with_formals ~with_locals kf v =
-  let open Cil_types in
-  Base.is_global v
-  ||
-  (match with_formals, with_locals, kf.fundec with
-   | false, false, _ | false, _, Declaration _ -> false
-   | true,  false, Definition (fundec,_) -> Base.is_formal v fundec
-   | false, true, Definition (fundec, _) -> Base.is_local v fundec
-   | true,  true, Definition (fundec, _) -> Base.is_formal_or_local v fundec
-   | true , _, Declaration (_, vd, _, _) -> Base.is_formal_of_prototype v vd)
-  || is_local_or_formal_of_caller v kf
-
-let _accept_base =
-  Dynamic.register
-    ~comment:"Returns [true] if the given base is a global, \
-              or a formal or local of either [kf] or one of its callers"
-    ~plugin:Options.name
-    "accept_base"
-    Datatype.(func2 Kernel_function.ty Base.ty bool)
-    (fun kf b -> accept_base ~with_formals:true ~with_locals:true kf b)
-
 let nb_calls () =
   let g = Cg.get () in
   (* [g] contains bidirectional edges (from caller to callee and
diff --git a/src/plugins/callgraph/uses.mli b/src/plugins/callgraph/uses.mli
index 9b4bdecf96a2bb7f674580c97f690d58144d2474..15d2441be9f4af3c969c94ef9dec5553ffef102d 100644
--- a/src/plugins/callgraph/uses.mli
+++ b/src/plugins/callgraph/uses.mli
@@ -38,17 +38,6 @@ val iter_on_callees : (Kernel_function.t -> unit) -> Kernel_function.t -> unit
 (** Iterate over all the callees of a given function in a (reverse) depth-first
     way. Do nothing if the function is not in the callgraph. *)
 
-val accept_base :
-  with_formals:bool ->
-  with_locals:bool ->
-  Kernel_function.t ->
-  Base.t ->
-  bool
-(** [accept_base formals locals kf b] returns [true] if and only if [b] is
-    - a global
-    - a formal or local of one of the callers of [kf]
-    - a formal or local of [kf] and the corresponding argument is [true]. *)
-
 val nb_calls: unit -> int
 (** @return the number of function calls in the whole callgraph. It is not
     (necessarily) equal to the number of graph edges (depending on the
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 1e42c4a3437f7961812f4e9d01e9280b3601b351..db84313b85ad427fb3c61cacc7507d1c02809886 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -708,6 +708,14 @@ module Logic_inout: sig
   val verify_assigns:
     Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
 
+
+  (** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
+      - a global
+      - a formal or local of one of the callers of [kf]
+      - a formal or local of [kf] and the corresponding argument is [true]. *)
+  val accept_base:
+    formals:bool -> locals:bool -> Kernel_function.t -> Base.t -> bool
+
 end
 
 module Eva_results: sig
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 0f0abc9a948c735208a91819a27f9e7c663c56e1..6dca30d2ccbd4b4f031acc222c6c5018ed26f9de 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -571,13 +571,14 @@ module State = struct
 
   let display_results () =
     Self.result "====== VALUES COMPUTED ======";
-    Eva_dynamic.Callgraph.iter_in_rev_order display;
+    if Plugin.is_present "inout"
+    && Self.is_debug_key_enabled Self.dkey_final_states
+    then Eva_dynamic.Callgraph.iter_in_rev_order display;
     Self.result "%t" Eva_perf.display
 
   let post_analysis _state =
     if Parameters.ForceValues.get ()
     && Self.verbose_atleast 1
-    && Plugin.is_present "inout"
     then Parameters.ForceValues.output display_results
 end
 
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index 9ad6ab5e069d3181be5fd3e378901aa793f0ad0a..9e641c47631d8bb00a3a77537d174723b84387de 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -80,6 +80,13 @@ let callsites kf =
     List.map (fun (kf, set) -> kf, StmtSet.elements set) calls
   with Not_found -> []
 
+let nb_callsites () =
+  CallersTable.fold
+    (fun _kf callers count ->
+       Kernel_function.Map.fold
+         (fun _caller callsites count -> count + StmtSet.cardinal callsites)
+         callers count)
+    0
 
 type analysis_target =
   [ `Builtin of string * Builtins.builtin * cacheable * funspec
diff --git a/src/plugins/eva/engine/function_calls.mli b/src/plugins/eva/engine/function_calls.mli
index d0381ea9eb1aaf6f9ba91db7b05d06d8b995aad4..58b10813a22cbce7b106f8308511f8e97612145a 100644
--- a/src/plugins/eva/engine/function_calls.mli
+++ b/src/plugins/eva/engine/function_calls.mli
@@ -60,6 +60,9 @@ val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
     of callsites (the call statements) inside. *)
 val callsites: kernel_function -> (kernel_function * stmt list) list
 
+(** Returns the number of callsites that have been analyzed. *)
+val nb_callsites: unit -> int
+
 
 type results = Complete | Partial | NoResults
 type analysis_status =
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index 9ad72ddf6f775bcb68f9b8ca3406688ccf39c4ba..4289d6ee4310ab68a556a5cf4165129587a3a308 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -228,7 +228,7 @@ let gui_compute_values (main_ui:main_ui) =
 
 let cleaned_outputs kf s =
   let outs = Db.Outputs.kinstr (Kstmt s) in
-  let accept = Eva_dynamic.Callgraph.accept_base kf in
+  let accept = Logic_inout.accept_base ~formals:true ~locals:true kf in
   let filter = Locations.Zone.filter_base accept in
   Option.map filter outs
 
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 959dab9ce2a4dc92f44f8ebb1bd5f00fd8378c8b..6739454077a4edb23a034a14bd1ab6582be8bea6 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -290,3 +290,40 @@ let verify_assigns kf ~pre froms =
   in
   let ab = Active_behaviors.create eval_predicate funspec in
   check_fct_assigns kf ab ~pre_state:pre froms
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utilitary function for Inout and From plugins                      --- *)
+(* -------------------------------------------------------------------------- *)
+
+let compute_all_callers kf =
+  let rec add_callers kf acc =
+    List.fold_left add_kf acc (Function_calls.callers kf)
+  and add_kf acc kf =
+    if Kernel_function.Hptset.mem kf acc
+    then acc
+    else add_callers kf (Kernel_function.Hptset.add kf acc)
+  in
+  add_callers kf (Kernel_function.Hptset.empty)
+
+let is_local_or_formal_of_caller callers base =
+  match Kernel_function.find_defining_kf (Base.to_varinfo base) with
+  | Some kf -> Kernel_function.Hptset.mem kf callers
+  | None | exception Base.Not_a_C_variable -> false
+
+let is_formal kf base =
+  match kf.fundec with
+  | Definition (fundec, _) -> Base.is_formal base fundec
+  | Declaration (_, vi, _, _) -> Base.is_formal_of_prototype base vi
+
+let is_local kf base =
+  match kf.fundec with
+  | Definition (fundec, _) -> Base.is_local base fundec
+  | Declaration _ -> false
+
+let accept_base ~formals ~locals kf =
+  let all_callers = compute_all_callers kf in
+  fun base ->
+    Base.is_global base
+    || (formals && is_formal kf base)
+    || (locals && is_local kf base)
+    || is_local_or_formal_of_caller all_callers base
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 3e2ab017cb3a65927c436e041196d1ff1bd0ebc9..9ed96ed03ade8bc969f784768289f74663412b07 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -73,4 +73,12 @@ val assigns_tlval_to_zones:
 val verify_assigns:
   Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
 
+
+(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
+    - a global
+    - a formal or local of one of the callers of [kf]
+    - a formal or local of [kf] and the corresponding argument is [true]. *)
+val accept_base:
+  formals:bool -> locals:bool -> Kernel_function.t -> Base.t -> bool
+
 [@@@ api_end]
diff --git a/src/plugins/eva/utils/eva_dynamic.ml b/src/plugins/eva/utils/eva_dynamic.ml
index 0de9bda0b047d3885410631bd1b908a4ec0db353..ebfdc9384ad7969a7b94b12b290d03c92ccc47f0 100644
--- a/src/plugins/eva/utils/eva_dynamic.ml
+++ b/src/plugins/eva/utils/eva_dynamic.ml
@@ -29,13 +29,12 @@ module Callgraph = struct
 
   let iter_in_rev_order f =
     let fallback = Globals.Functions.iter in
-    let typ = Datatype.(func (func Kernel_function.ty unit) unit) in
-    get ~plugin "iter_in_rev_order" typ ~fallback f
-
-  let accept_base kf v =
-    let fallback _ _ = true in
-    let typ = Datatype.(func2 Kernel_function.ty Base.ty bool) in
-    get ~plugin "accept_base" typ ~fallback kf v
+    (* callgraph is too slow on programs with too many callsites. *)
+    if Function_calls.nb_callsites () > 20000
+    then fallback f
+    else
+      let typ = Datatype.(func (func Kernel_function.ty unit) unit) in
+      get ~plugin "iter_in_rev_order" typ ~fallback f
 end
 
 module Scope = struct
diff --git a/src/plugins/eva/utils/eva_dynamic.mli b/src/plugins/eva/utils/eva_dynamic.mli
index 59f90d06ba5130c566f07d7e2bc56a4e5bab6a82..ce85b848b62ff215ef2dc611426d07c83ede0d58 100644
--- a/src/plugins/eva/utils/eva_dynamic.mli
+++ b/src/plugins/eva/utils/eva_dynamic.mli
@@ -24,12 +24,9 @@
 
 module Callgraph: sig
   (** Iterates over all functions in the callgraph in reverse order, i.e. from
-      callees to callers. If callgraph is missing, the order is unspecified. *)
+      callees to callers. If callgraph is missing or if the number of callsites
+      is too big, the order is unspecified. *)
   val iter_in_rev_order: (Kernel_function.t -> unit) -> unit
-
-  (** Returns [true] if [base] is a global, or a formal or local of either [kf]
-      or one of its callers. If callgraph is missing, always returns true. *)
-  val accept_base: Kernel_function.t -> Base.t -> bool
 end
 
 module Scope: sig
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index 0dbc329585349f3aa32ddb899bdfb04ff82c4b82..3c28cfb69da993bfc8f99d62ffb18c3c4647359f 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -36,6 +36,7 @@ module Eval_op = Eval_op
 module Eval_terms = Eval_terms
 module Eval_typ = Eval_typ
 module Function_calls = Function_calls
+module Logic_inout = Logic_inout
 module Main_locations = Main_locations
 module Main_values = Main_values
 module Parameters = Parameters
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 941329f7b5963059e37c64632b7cadcb89531718..2012d89d2920890ab2e46f43185c330c2c050d7f 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -40,6 +40,7 @@ module Eval_op = Eval_op
 module Eval_terms = Eval_terms
 module Eval_typ = Eval_typ
 module Function_calls = Function_calls
+module Logic_inout = Logic_inout
 module Main_locations = Main_locations
 module Main_values = Main_values
 module Parameters = Parameters
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 4f2754d424fc30b0e4b77db503d08910f64c68e1..484fbdba5b54ddcd4643bbba1f7f7e62d396d3e6 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -50,14 +50,17 @@ module To_Use = struct
   let get_from_call kf _ = memo kf
 
   let keep_base kf = (* Eta-expansion required *)
-    Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf
+    Eva.Logic_inout.accept_base ~formals:false ~locals:false kf
 
   let cleanup kf froms =
     if Function_Froms.Memory.is_bottom froms.Function_Froms.deps_table
     then froms
     else
+      let accept_base =
+        Eva.Logic_inout.accept_base ~formals:true ~locals:false kf
+      in
       let f b intervs =
-        if Callgraph.Uses.accept_base ~with_formals:true ~with_locals:false kf b
+        if accept_base b
         then Zone.inject b intervs
         else Zone.bottom
       in
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index aca0e52ddd2965f28b1314938435ef589451e60f..1de8961fa3ebe407c16537cbf034c4663c99b7cc 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -155,12 +155,12 @@ let get_external =
   Externals.memo
     (fun kf ->
        Zone.filter_base
-         (Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf)
+         (Eva.Logic_inout.accept_base ~formals:false ~locals:false kf)
          (get_internal kf))
 
 let get_with_formals kf =
   Zone.filter_base
-    (Callgraph.Uses.accept_base ~with_formals:true ~with_locals:false kf)
+    (Eva.Logic_inout.accept_base ~formals:true ~locals:false kf)
     (get_internal kf)
 
 let compute_external kf = ignore (get_external kf)
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index c05eda0496ba541c53f4c06ae3456f915dc31fce..d3240b5f5a6713dccf230a2a31951d017fd9c6b1 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -94,7 +94,7 @@ let join_and_is_included smaller larger =
 
 let externalize_zone ~with_formals kf =
   Zone.filter_base
-    (Callgraph.Uses.accept_base ~with_formals ~with_locals:false kf)
+    (Eva.Logic_inout.accept_base ~formals:with_formals ~locals:false kf)
 
 (* This code evaluates an assigns, computing in particular a sound approximation
    of sure outputs. For an assigns [locs_out \from locs_from], the process
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 9f9974b7118e3b1635fd26546f9c44d15fb00e40..14c8ee4b6bf404a0c0a29ffafcbf4f8681474dd9 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -117,7 +117,7 @@ class virtual do_it_ = object(self)
 
   method clean_kf_result kf r =
     Zone.filter_base
-      (Callgraph.Uses.accept_base ~with_formals:true ~with_locals:true kf)
+      (Eva.Logic_inout.accept_base ~formals:true ~locals:true kf)
       r
 
   method compute_funspec kf =
@@ -141,7 +141,7 @@ let get_internal = Analysis.kernel_function
 
 let externalize kf x =
   Zone.filter_base
-    (Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf)
+    (Eva.Logic_inout.accept_base ~formals:false ~locals:false kf)
     x
 
 module Externals =