diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 1a19ba3926ebeb591bac02fb259657b22c9332d1..0a16b809c69db96209c84ba1bff1d55e61f109c4 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -615,6 +615,7 @@ let loc_of_typoffset b typ offset =
   with SizeOfError _ as _e ->
     make_loc (Location_Bits.inject b Ival.top) Int_Base.top
 
+let loc_top = make_loc Location_Bits.top Int_Base.top
 let loc_bottom = make_loc Location_Bits.bottom Int_Base.top
 let is_bottom_loc l = Location_Bits.(equal l.loc bottom)
 
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 632cbb17a31e507e2c1a80c3d9d524197fde6615..00b3749be4659ae9db24070e426659bc486485d3 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -332,6 +332,7 @@ type location = private {
 (** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
 module Location: Datatype.S with type t = location
 
+val loc_top : location
 val loc_bottom : location
 val is_bottom_loc: location -> bool
 
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index f1ad02b3417900d1d66ec1f5df37d6e879d75aac..60dd3d6ff3186689da16f1b7bb285ba49d78ff7c 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -53,7 +53,9 @@ let show_non_det_state fmt state =
     (* TODO: sync Data_for_aorai.get_state_var with current project*)
     let vi = Data_for_aorai.get_varinfo s.Promelaast.name in
     let e = Cil.evar vi in
-    let cvalue = !Db.Value.eval_expr state e in
+    let cvalue =
+      Eva.Results.(in_cvalue_state state |> eval_exp e |> as_cvalue)
+    in
     if Cvalue.V.contains_non_zero cvalue then
       print_state s (not (Cvalue.V.contains_zero cvalue))
   in
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 6a5fa5a46c74429289505c3fa8d042dc0667d1cc..9b3a2e7c79e8c9d2611abc9ecfc79c1b7b5a28d9 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -85,8 +85,7 @@ struct
     before_kinstr kinstr |> eval_lval lval |> as_cvalue
 
   let to_location kinstr lval =
-    before_kinstr kinstr |> eval_address lval |> as_location |>
-    Result.value ~default:Locations.loc_bottom
+    before_kinstr kinstr |> eval_address lval |> as_location
 
   let to_zone kinstr lval =
     before_kinstr kinstr |> eval_address lval |> as_zone
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index fc8896e0d68517d862d8a0670e7605de21fff13f..5fc9ded3be8d4c07e658455346c9484de411fab1 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -68,6 +68,9 @@ module Analysis: sig
       finishes. If [on] is given, the hook will only be called when the
       analysis switches to this specific state. *)
 
+  val emitter: Emitter.t
+  (** Emitter used by Eva to emit property statuses. *)
+
   (** Kind of results for the analysis of a function body. *)
   type results =
     | Complete
@@ -153,7 +156,7 @@ module Results: sig
         function body: all requests in the function will lead to a Bottom error.
       - results have not been saved, due to the [-eva-no-results] parameter:
         all requests in the function will lead to a Top error. *)
-  val are_available: Cil_types.kernel_function -> bool
+  val are_available : Cil_types.kernel_function -> bool
 
   type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
 
@@ -209,6 +212,11 @@ module Results: sig
   (** Just before a statement or at the start of the analysis. *)
   val before_kinstr : Cil_types.kinstr -> request
 
+  (** Evaluation in a given cvalue state. Callstacks selection are silently
+      ignored on such requests. For internal use, could be modified or removed
+      in a future version. *)
+  val in_cvalue_state : Cvalue.Model.t -> request
+
 
   (** Callstack selection *)
 
@@ -257,7 +265,7 @@ module Results: sig
       request. If [filter] is provided, states are filtered on the given bases
       (for domains that support this feature).
       Returns a list of pair (name, state) for all available domains. *)
-  val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
+  val print_states : ?filter:Base.Hptset.t -> request -> (string * string) list
 
   (** Dependencies *)
 
@@ -273,6 +281,17 @@ module Results: sig
       evaluate the given lvalue, excluding the lvalue zone itself. *)
   val address_deps : Cil_types.lval -> request -> Locations.Zone.t
 
+  (** Memory dependencies of an expression. *)
+  type deps = Function_Froms.Deps.deps = {
+    data: Locations.Zone.t;
+    (** Memory zone directly required to evaluate the given expression. *)
+    indirect: Locations.Zone.t;
+    (** Memory zone read to compute data addresses. *)
+  }
+
+  (** Computes (an overapproximation of) the memory dependencies of an
+      expression. *)
+  val expr_dependencies : Cil_types.exp -> request -> deps
 
   (** Evaluation *)
 
@@ -335,16 +354,28 @@ module Results: sig
   val as_cvalue_or_uninitialized : value evaluation -> Cvalue.V_Or_Uninitialized.t
 
 
+  (** Converts into a C location abstraction. Error cases are converted into
+      bottom or top locations accordingly. *)
+  val as_location : address evaluation -> Locations.location
+
   (** Converts into a C location abstraction. *)
-  val as_location : address evaluation -> Locations.location result
+  val as_location_result : address evaluation -> Locations.location result
 
   (** Converts into a Zone. Error cases are converted into bottom or top zones
       accordingly. *)
-  val as_zone: address evaluation -> Locations.Zone.t
+  val as_zone : address evaluation -> Locations.Zone.t
 
   (** Converts into a Zone result. *)
   val as_zone_result : address evaluation -> Locations.Zone.t result
 
+  (** Converts into a C location abstraction. Error cases are converted into
+      bottom or top locations accordingly. *)
+  val as_precise_loc : address evaluation -> Precise_locs.precise_location
+
+  (** Converts into a C location abstraction. *)
+  val as_precise_loc_result :
+    address evaluation -> Precise_locs.precise_location result
+
 
   (** Evaluation properties *)
 
@@ -380,7 +411,7 @@ module Results: sig
       the main function has been analyzed for [Kglobal]. *)
   val is_reachable_kinstr : Cil_types.kinstr -> bool
 
-  val condition_truth_value: Cil_types.stmt -> bool * bool
+  val condition_truth_value : Cil_types.stmt -> bool * bool
   (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
       (resp. snd) is true if and only if the condition of the 'if' has been
       evaluated to true (resp. false) at least once during the analysis. *)
@@ -564,7 +595,10 @@ end
 module Cvalue_callbacks: sig
 
   (** Register actions to performed during the Eva analysis,
-      with access to the states of the cvalue domain. *)
+      with access to the states of the cvalue domain.
+      This API is for internal use only, and may be modified or removed
+      in a future version. Please contact us if you need to register callbacks
+      to be executed during an Eva analysis. *)
 
   type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
   type state = Cvalue.Model.t
@@ -605,18 +639,49 @@ module Cvalue_callbacks: sig
 
 end
 
-module Eval_terms: sig
+module Logic_inout: sig
 
-  (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
-      to evaluate the predicate [p] in a code annotation in cvalue state [here],
-      in a function whose pre-state is [pre].
+  (** Functions used by the Inout and From plugins to interpret predicate
+      and assigns clauses. This API may change according to these plugins
+      development. *)
+
+  (** [predicate_deps ~pre ~here p] computes the logic dependencies needed
+      to evaluate the predicate [p] in cvalue state [here], in a function
+      whose pre-state is [pre].
       Returns None on either an evaluation error or on unsupported construct. *)
-  val annot_predicate_deps:
+  val predicate_deps:
     pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
     Cil_types.predicate -> Locations.Zone.t option
+
+  (** Returns the list of behaviors of the given function that are active for
+      the given initial state. *)
+  val valid_behaviors:
+    Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+  (** Evaluation of the memory zone read by the \from part of an assigns clause,
+      in the given cvalue state.  *)
+  val assigns_inputs_to_zone:
+    Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+  (** Evaluation of the memory zone written by an assigns clauses, in the given
+      cvalue state. *)
+  val assigns_outputs_to_zone:
+    result: Cil_types.varinfo option ->
+    Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+  (** Evaluate the assigns clauses of the given function in its given pre-state,
+      and compare them with the given froms (computed by the from plugin).
+      Emits warnings if needed, and sets statuses to the assigns clauses. *)
+  val verify_assigns:
+    Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+
 end
 
 module Eva_results: sig
+
+  (** Internal temporary API: please do not use it, as it should be removed in a
+      future version. *)
+
   type results
 
   val get_results: unit -> results
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 502fec6d6edf50ebae146a7f34a37b63502fcad6..771f0d370a7ef9ea85f2b87dc2a5c606d4f71418 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -99,6 +99,6 @@
   gen-api.sh Eva.header
   engine/analysis.mli utils/results.mli parameters.mli
   utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
-  utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli
+  utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli
   utils/unit_tests.mli)
  (action (run %{deps})))
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 2b63e58b9f02008b7c7a865bc8a44dc2e540140a..f1fc2d5ff1ed3d2b1f99acaf51d0e0815518134c 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -29,6 +29,7 @@ let current_computation_state = Self.current_computation_state
 let register_computation_hook = Self.register_computation_hook
 let is_computed = Self.is_computed
 let self = Self.state
+let emitter = Eva_utils.emitter
 
 type results = Function_calls.results = Complete | Partial | NoResults
 type status = Function_calls.analysis_status =
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index cd472bcd27b2e9f8b29a4c1c8e763b1fcf10710b..be2d743c970b9b935bff2fb5bfa5b2f260628f01 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -108,6 +108,9 @@ val register_computation_hook: ?on:computation_state ->
     finishes. If [on] is given, the hook will only be called when the
     analysis switches to this specific state. *)
 
+val emitter: Emitter.t
+(** Emitter used by Eva to emit property statuses. *)
+
 (** Kind of results for the analysis of a function body. *)
 type results =
   | Complete
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index ae229527a499bc4e76e252368008be0047956ce1..8c46196981a35727588bc6efaec55c399cb301ca 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2745,17 +2745,6 @@ and predicate_deps env pred =
   try Some (do_eval env pred)
   with LogicEvalError _ -> None
 
-let annot_predicate_deps ~pre ~here predicate =
-  let env = env_annot ~pre ~here () in
-  let logic_deps = predicate_deps env predicate in
-  let join logic_deps =
-    Cil_datatype.Logic_label.Map.fold
-      (fun _ -> Locations.Zone.join)
-      logic_deps
-      Locations.Zone.bottom
-  in
-  Option.map join logic_deps
-
 (* -------------------------------------------------------------------------- *)
 (* --- Export                                                             --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/legacy/eval_terms.mli b/src/plugins/eva/legacy/eval_terms.mli
index 95e826556e32e440404e88b6fc1c057993778897..a8b326ffc3dbb4651441e06591a75a501a4b3130 100644
--- a/src/plugins/eva/legacy/eval_terms.mli
+++ b/src/plugins/eva/legacy/eval_terms.mli
@@ -118,16 +118,3 @@ val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
 
 val reduce_by_predicate :
   eval_env -> bool -> predicate -> eval_env
-
-
-
-[@@@ api_start]
-
-(** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
-    to evaluate the predicate [p] in a code annotation in cvalue state [here],
-    in a function whose pre-state is [pre].
-    Returns None on either an evaluation error or on unsupported construct. *)
-val annot_predicate_deps:
-  pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
-  Cil_types.predicate -> Locations.Zone.t option
-[@@@ api_end]
diff --git a/src/plugins/eva/domains/cvalue/cvalue_specification.ml b/src/plugins/eva/legacy/logic_inout.ml
similarity index 74%
rename from src/plugins/eva/domains/cvalue/cvalue_specification.ml
rename to src/plugins/eva/legacy/logic_inout.ml
index aebbdbd39bcbf3bd9e84a94dc30a53652b3deaf3..98803359c8570b7c958d8e5e455be5af70710e12 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -22,6 +22,79 @@
 
 open Cil_types
 
+let predicate_deps ~pre ~here predicate =
+  let env = Eval_terms.env_annot ~pre ~here () in
+  let logic_deps = Eval_terms.predicate_deps env predicate in
+  let join logic_deps =
+    Cil_datatype.Logic_label.Map.fold
+      (fun _ -> Locations.Zone.join)
+      logic_deps
+      Locations.Zone.bottom
+  in
+  Option.map join logic_deps
+
+let valid_behaviors kf state =
+  let funspec = Annotations.funspec kf in
+  let eval_predicate pred =
+    match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
+    | True -> Alarmset.True
+    | False -> Alarmset.False
+    | Unknown -> Alarmset.Unknown
+  in
+  let ab = Active_behaviors.create eval_predicate funspec in
+  Active_behaviors.active_behaviors ab
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute inout from assigns clauses                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let eval_error_reason fmt e =
+  if e <> Eval_terms.CAlarm
+  then Eval_terms.pretty_logic_evaluation_error fmt e
+
+let eval_tlval_as_zone assigns kind env acc t =
+  try
+    let alarm_mode = Eval_terms.Ignore in
+    let zone = Eval_terms.eval_tlval_as_zone ~alarm_mode kind env t.it_content in
+    Locations.Zone.join acc zone
+  with Eval_terms.LogicEvalError e ->
+    let pp_clause fmt =
+      if kind = Read
+      then Printer.pp_from fmt assigns
+      else Printer.pp_term fmt (fst assigns).it_content
+    in
+    Self.warning ~current:true ~once:true
+      "Failed to interpret %sassigns clause '%t'%a"
+      (if kind = Read then "inputs in " else "")
+      pp_clause eval_error_reason e;
+    Locations.Zone.top
+
+let assigns_inputs_to_zone state assigns =
+  let env = Eval_terms.env_assigns ~pre:state in
+  let treat_asgn acc (_,ins as asgn) =
+    match ins with
+    | FromAny -> Locations.Zone.top
+    | From l -> List.fold_left (eval_tlval_as_zone asgn Read env) acc l
+  in
+  match assigns with
+  | WritesAny -> Locations.Zone.top
+  | Writes l  -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+let assigns_outputs_to_zone ~result state assigns =
+  let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
+  let treat_asgn acc (out,_ as asgn) =
+    if Logic_utils.is_result out.it_content && result = None
+    then acc
+    else eval_tlval_as_zone asgn Write env acc out
+  in
+  match assigns with
+  | WritesAny -> Locations.Zone.top
+  | Writes l  -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+(* -------------------------------------------------------------------------- *)
+(* --- Verify assigns clauses                                             --- *)
+(* -------------------------------------------------------------------------- *)
+
 (* Eval: under-approximation of the term.  Note that ACSL states
    that assigns clauses are evaluated in the pre-state.
    We skip [\result]: it is meaningless when evaluating the 'assigns' part,
@@ -176,7 +249,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
          List.iter2 check_from assigns_deps assigns_zones)
   in List.iter check_for_behavior behaviors
 
-let verify_assigns_from kf ~pre froms =
+let verify_assigns kf ~pre froms =
   let funspec = Annotations.funspec kf in
   let env = Eval_terms.env_pre_f ~pre () in
   let eval_predicate pred =
@@ -186,6 +259,4 @@ let verify_assigns_from kf ~pre froms =
     | Eval_terms.Unknown -> Alarmset.Unknown
   in
   let ab = Active_behaviors.create eval_predicate funspec in
-  check_fct_assigns kf ab ~pre_state:pre froms;;
-
-Db.Value.verify_assigns_froms := verify_assigns_from;;
+  check_fct_assigns kf ab ~pre_state:pre froms
diff --git a/src/plugins/eva/domains/cvalue/cvalue_specification.mli b/src/plugins/eva/legacy/logic_inout.mli
similarity index 51%
rename from src/plugins/eva/domains/cvalue/cvalue_specification.mli
rename to src/plugins/eva/legacy/logic_inout.mli
index 7af69cb1ef9e1fab669041eca3639b4cb9f3ba3c..92d6afd81687589a37b2bfbdcadea6bfe67a6cba 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_specification.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -20,4 +20,40 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** No function exported. Registers Db.Value.verify_assigns_from. *)
+[@@@ api_start]
+
+(** Functions used by the Inout and From plugins to interpret predicate
+    and assigns clauses. This API may change according to these plugins
+    development. *)
+
+(** [predicate_deps ~pre ~here p] computes the logic dependencies needed
+    to evaluate the predicate [p] in cvalue state [here], in a function
+    whose pre-state is [pre].
+    Returns None on either an evaluation error or on unsupported construct. *)
+val predicate_deps:
+  pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+  Cil_types.predicate -> Locations.Zone.t option
+
+(** Returns the list of behaviors of the given function that are active for
+    the given initial state. *)
+val valid_behaviors:
+  Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+(** Evaluation of the memory zone read by the \from part of an assigns clause,
+    in the given cvalue state.  *)
+val assigns_inputs_to_zone:
+  Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+(** Evaluation of the memory zone written by an assigns clauses, in the given
+    cvalue state. *)
+val assigns_outputs_to_zone:
+  result: Cil_types.varinfo option ->
+  Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+(** Evaluate the assigns clauses of the given function in its given pre-state,
+    and compare them with the given froms (computed by the from plugin).
+    Emits warnings if needed, and sets statuses to the assigns clauses. *)
+val verify_assigns:
+  Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+
+[@@@ api_end]
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
index e48168230e40b04321390fa52dde2dbc0b2e9907..197393e0a5592251d9aaf9201d072a6e3617a309 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -34,76 +34,6 @@ let main () =
 let () = Db.Main.extend main
 
 
-(* Functions to register in Db.Value *)
-
-let eval_error_reason fmt e =
-  if e <> Eval_terms.CAlarm
-  then Eval_terms.pretty_logic_evaluation_error fmt e
-
-let assigns_inputs_to_zone state assigns =
-  let env = Eval_terms.env_assigns ~pre:state in
-  let treat_asgn acc (_,ins as asgn) =
-    match ins with
-    | FromAny -> Zone.top
-    | From l ->
-      try
-        List.fold_left
-          (fun acc t ->
-             let z =
-               Eval_terms.eval_tlval_as_zone ~alarm_mode:Eval_terms.Ignore
-                 Read env t.it_content
-             in
-             Zone.join acc z)
-          acc
-          l
-      with Eval_terms.LogicEvalError e ->
-        Self.warning ~current:true ~once:true
-          "Failed to interpret inputs in assigns clause '%a'%a"
-          Printer.pp_from asgn eval_error_reason e;
-        Zone.top
-  in
-  match assigns with
-  | WritesAny -> Zone.top
-  | Writes l  -> List.fold_left treat_asgn Zone.bottom l
-
-let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
-  let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
-  let treat_asgn acc ({it_content = out},_) =
-    if Logic_utils.is_result out && result = None
-    then acc
-    else
-      try
-        let z = eval env out in
-        join z acc
-      with Eval_terms.LogicEvalError e ->
-        Self.warning ~current:true ~once:true
-          "Failed to interpret assigns clause '%a'%a"
-          Printer.pp_term out eval_error_reason e;
-        join top acc
-  in
-  match assigns with
-  | WritesAny -> join top bot
-  | Writes l  -> List.fold_left treat_asgn bot l
-
-let assigns_outputs_to_zone =
-  let eval env term =
-    Eval_terms.eval_tlval_as_zone
-      ~alarm_mode:Eval_terms.Ignore Write env term
-  in
-  assigns_outputs_aux ~eval
-    ~bot:Locations.Zone.bottom ~top:Locations.Zone.top ~join:Locations.Zone.join
-
-let assigns_outputs_to_locations =
-  let eval env term =
-    Eval_terms.eval_tlval_as_location
-      ~alarm_mode:Eval_terms.Ignore env term
-  in
-  assigns_outputs_aux
-    ~eval
-    ~bot:[] ~top:(Locations.make_loc Locations.Location_Bits.top Int_Base.top)
-    ~join:(fun v l -> v :: l)
-
-
 (* "access" functions before evaluation, registered in Db.Value *)
 let access_value_of_lval kinstr lv =
   let state = Db.Value.get_state kinstr in
@@ -132,30 +62,19 @@ let eval_predicate ~pre ~here p =
   | False -> Property_status.False_if_reachable
   | Unknown -> Property_status.Dont_know
 
-let valid_behaviors kf state =
-  let funspec = Annotations.funspec kf in
-  let eval_predicate pred =
-    match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
-    | Eval_terms.True -> Alarmset.True
-    | Eval_terms.False -> Alarmset.False
-    | Eval_terms.Unknown -> Alarmset.Unknown
-  in
-  let ab = Active_behaviors.create eval_predicate funspec in
-  Active_behaviors.active_behaviors ab
-
 let () =
   Db.Value.is_called := Function_calls.is_called;
   Db.Value.callers := Function_calls.callsites;
   Db.Value.use_spec_instead_of_definition :=
     Function_calls.use_spec_instead_of_definition;
-  Db.Value.assigns_outputs_to_zone := assigns_outputs_to_zone;
-  Db.Value.assigns_outputs_to_locations := assigns_outputs_to_locations;
-  Db.Value.assigns_inputs_to_zone := assigns_inputs_to_zone;
+  Db.Value.assigns_outputs_to_zone :=
+    (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
+  Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
   Db.Value.access := access_value_of_lval;
   Db.Value.access_location := access_value_of_location;
   Db.Value.access_expr := access_value_of_expr;
   Db.Value.Logic.eval_predicate := eval_predicate;
-  Db.Value.valid_behaviors := valid_behaviors;
+  Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
   Db.From.find_deps_term_no_transitivity_state :=
     find_deps_term_no_transitivity_state;
 
@@ -505,6 +424,8 @@ let register (module Eval: Eval) (module Export: Export) =
 
 let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state
 
+let () = Db.Value.verify_assigns_froms := Logic_inout.verify_assigns
+
 let () =
   let eval = (module Eval : Eval) in
   let export = (module Export ((val eval : Eval)) : Export) in
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index cb26f37aa10beb18fff6f8edc4f9e4eaff19445c..3122b1b3c6554bb3e68d48c5cc320016cc2149cc 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -23,7 +23,10 @@
 [@@@ api_start]
 
 (** Register actions to performed during the Eva analysis,
-    with access to the states of the cvalue domain. *)
+    with access to the states of the cvalue domain.
+    This API is for internal use only, and may be modified or removed
+    in a future version. Please contact us if you need to register callbacks
+    to be executed during an Eva analysis. *)
 
 type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
 type state = Cvalue.Model.t
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index 6144615c2e453f9366bd1c1c096c4418784439ab..19e35f6bd7b67061ba4db590f2d0f1ea614690bf 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -30,6 +30,10 @@ val is_non_terminating_instr: stmt -> bool
 (** {2 Results} *)
 
 [@@@ api_start]
+
+(** Internal temporary API: please do not use it, as it should be removed in a
+    future version. *)
+
 type results
 
 val get_results: unit -> results
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 4f28347df9aabdbb1b256d5f27b248070e4d4a5b..7717dfaf3dbd739795331c642429f2ac563bf357 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -274,42 +274,58 @@ let dump_garbled_mix () =
       (Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep:"@ " pp_one) l
 
 
+type deps = Function_Froms.Deps.deps = {
+  data: Locations.Zone.t;
+  indirect: Locations.Zone.t;
+}
+
+let bottom_deps =
+  { data = Locations.Zone.bottom; indirect = Locations.Zone.bottom }
+
+let join_deps a b =
+  { data = Locations.Zone.join a.data b.data;
+    indirect = Locations.Zone.join a.indirect b.indirect; }
+
+let deps_to_zone deps = Locations.Zone.join deps.data deps.indirect
+
 (* Computation of the inputs of an expression. *)
-let rec zone_of_expr find_loc expr =
+let rec deps_of_expr find_loc expr =
   let rec process expr = match expr.enode with
     | Lval lval ->
       (* Dereference of an lvalue. *)
-      zone_of_lval find_loc lval
+      deps_of_lval find_loc lval
     | UnOp (_, e, _) | CastE (_, e) ->
       (* Unary operators. *)
       process e
     | BinOp (_, e1, e2, _) ->
       (* Binary operators. *)
-      Locations.Zone.join (process e1) (process e2)
+      join_deps (process e1) (process e2)
     | StartOf lv | AddrOf lv ->
       (* computation of an address: the inputs of the lvalue whose address
          is computed are read to compute said address. *)
-      indirect_zone_of_lval find_loc lv
+      { data = indirect_zone_of_lval find_loc lv;
+        indirect = Locations.Zone.bottom; }
     | Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | AlignOfE _ ->
       (* static constructs, nothing is read to evaluate them. *)
-      Locations.Zone.bottom
+      bottom_deps
   in
   process expr
 
+and zone_of_expr find_loc expr = deps_to_zone (deps_of_expr find_loc expr)
+
 (* dereference of an lvalue: first, its address must be computed,
    then its contents themselves are read *)
-and zone_of_lval find_loc lval =
+and deps_of_lval find_loc lval =
   let ploc = find_loc lval in
-  let loc = Precise_locs.imprecise_location ploc in
-  let zone = Locations.(enumerate_valid_bits Read loc) in
-  Locations.Zone.join zone
-    (indirect_zone_of_lval find_loc lval)
+  let zone = Precise_locs.enumerate_valid_bits Read ploc in
+  { data = zone;
+    indirect = indirect_zone_of_lval find_loc lval; }
 
 (* Computations of the inputs of a lvalue : union of the "host" part and
    the offset. *)
 and indirect_zone_of_lval find_loc (lhost, offset) =
-  (Locations.Zone.join
-     (zone_of_lhost find_loc lhost) (zone_of_offset find_loc offset))
+  Locations.Zone.join
+    (zone_of_lhost find_loc lhost) (zone_of_offset find_loc offset)
 
 (* Computation of the inputs of a host. Nothing for a variable, and the
    inputs of [e] for a dereference [*e]. *)
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index be3385152b007307f1adab510474ed57dcc21d19..7f665f05f267b3873a053b923f5917eb5ee1526f 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -107,6 +107,17 @@ val indirect_zone_of_lval:
     on which the offset and the pointer expression (if any) of an lvalue depend.
 *)
 
+
+type deps = Function_Froms.Deps.deps = {
+  data: Locations.Zone.t;
+  indirect: Locations.Zone.t;
+}
+
+val deps_of_expr:
+  (lval -> Precise_locs.precise_location) -> exp -> deps
+(** Given a function computing the location of lvalues, computes the memory
+    dependencies of an expression. *)
+
 (** Computes the height of an expression, that is the maximum number of nested
     operations in this expression. *)
 val height_expr: exp -> int
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 56935b6b2281b2aaef1ea25d1ccc65ad6624b27c..c7b44e783a11eac858a3a04e99a7e9d4f670b308 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -39,12 +39,16 @@ type control_point =
   | Before of Cil_types.stmt
   | After of Cil_types.stmt
 
-type request = {
+type context = {
   control_point : control_point;
   selector : callstack list option;
   filter: (callstack -> bool) list;
 }
 
+type request =
+  | Point of context
+  | Cvalue of Cvalue.Model.t
+
 type error = Bottom | Top | DisabledDomain
 type 'a result = ('a,error) Result.t
 
@@ -61,11 +65,8 @@ let pretty_result f fmt r =
 
 (* Building requests *)
 
-let make control_point = {
-  control_point;
-  selector = None;
-  filter = [];
-}
+let make control_point =
+  Point { control_point; selector = None; filter = []; }
 
 let before stmt = make (Before stmt)
 let after stmt = make (After stmt)
@@ -78,9 +79,20 @@ let before_kinstr = function
   | Cil_types.Kglobal -> at_start
   | Kstmt stmt -> before stmt
 
-let in_callstacks l req = { req with selector = Some l }
-let in_callstack cs req = { req with selector = Some [cs] }
-let filter_callstack f req = { req with filter = f :: req.filter }
+let change_context f = function
+  | Point ctx -> Point (f ctx)
+  | Cvalue _ as x -> x
+
+let in_callstacks l =
+  change_context (fun ctx -> { ctx with selector = Some l })
+
+let in_callstack cs =
+  change_context (fun ctx -> { ctx with selector = Some [cs] })
+
+let filter_callstack f =
+  change_context (fun ctx -> { ctx with filter = f :: ctx.filter })
+
+let in_cvalue_state cvalue = Cvalue cvalue
 
 
 (* Manipulating request results *)
@@ -120,7 +132,7 @@ struct
     | `Top -> Top
     | `Value state -> ByCallstack [cs,state]
 
-  let by_callstack : request ->
+  let by_callstack : context ->
     [< `Bottom | `Top | `Value of 'a Value_types.Callstack.Hashtbl.t ] ->
     ('a, restricted_to_callstack) t =
     fun req -> function
@@ -212,49 +224,64 @@ struct
     | Address: (EvalTypes.loc, 'c) Response.t * Locations.access ->
         (address,'c) evaluation
 
-  let get_by_callstack (req : request) :
+  let get_from_cvalue cvalue =
+    if Cvalue.Model.(equal cvalue bottom)
+    then `Bottom
+    else if Cvalue.Model.(equal cvalue top)
+    then `Top
+    else
+      let state = cvalue, Locals_scoping.bottom () in
+      `Value (A.Dom.set Cvalue_domain.State.key state A.Dom.top)
+
+  let get_by_callstack (ctx : context) :
     (_, restricted_to_callstack) Response.t =
     let open Response in
-    let selection = req.selector in
-    match req.control_point with
+    let selection = ctx.selector in
+    match ctx.control_point with
     | Before stmt ->
       A.get_stmt_state_by_callstack ?selection ~after:false stmt
-      |> by_callstack req
+      |> by_callstack ctx
     | After stmt ->
       A.get_stmt_state_by_callstack ?selection ~after:true stmt
-      |> by_callstack req
+      |> by_callstack ctx
     | Initial ->
       A.get_global_state () |> singleton []
     | Start kf ->
-      A.get_initial_state_by_callstack ?selection kf |> by_callstack req
+      A.get_initial_state_by_callstack ?selection kf |> by_callstack ctx
 
   let get (req : request) : (_, unrestricted_response) Response.t =
-    if req.filter <> [] || Option.is_some req.selector then
-      Response.coercion @@ get_by_callstack req
-    else
-      let open Response in
-      let state =
-        match req.control_point with
-        | Before stmt -> A.get_stmt_state ~after:false stmt
-        | After stmt -> A.get_stmt_state ~after:true stmt
-        | Start kf -> A.get_initial_state kf
-        | Initial -> A.get_global_state ()
-      in
-      consolidated ~top:A.Dom.top state
+    let open Response in
+    match req with
+    | Cvalue state -> consolidated ~top:A.Dom.top  (get_from_cvalue state)
+    | Point req ->
+      if req.filter <> [] || Option.is_some req.selector then
+        Response.coercion @@ get_by_callstack req
+      else
+        let state =
+          match req.control_point with
+          | Before stmt -> A.get_stmt_state ~after:false stmt
+          | After stmt -> A.get_stmt_state ~after:true stmt
+          | Start kf -> A.get_initial_state kf
+          | Initial -> A.get_global_state ()
+        in
+        consolidated ~top:A.Dom.top state
 
   let convert : 'a or_top_bottom -> 'a result = function
     | `Top -> Result.error Top
     | `Bottom -> Result.error Bottom
     | `Value v -> Result.ok v
 
-  let callstacks req =
-    get_by_callstack req |> Response.callstacks
+  let callstacks = function
+    | Point ctx -> get_by_callstack ctx |> Response.callstacks
+    | Cvalue _ -> []
 
-  let by_callstack req =
-    let f cs _res acc =
-      (cs, in_callstack cs req) :: acc
-    in
-    get_by_callstack req |> Response.fold f []
+  let by_callstack = function
+    | Cvalue _ -> assert false
+    | Point ctx as req ->
+      let f cs _res acc =
+        (cs, in_callstack cs req) :: acc
+      in
+      get_by_callstack ctx |> Response.fold f []
 
   let is_reachable req =
     match get req with
@@ -396,6 +423,25 @@ struct
       in
       Response.map extract r, access
 
+  let as_precise_loc res =
+    match A.Loc.get Main_locations.PLoc.key with
+    | None ->
+      Result.error DisabledDomain
+    | Some get ->
+      let join ploc1 ploc2 =
+        if Precise_locs.equal_loc ploc1 ploc2 then ploc1 else
+          let loc1 = Precise_locs.imprecise_location ploc1
+          and loc2 = Precise_locs.imprecise_location ploc2 in
+          assert (Int_Base.equal loc1.size loc2.size);
+          let size = loc1.size in
+          let loc_bit = Locations.Location_Bits.join loc1.loc loc2.loc in
+          let ploc_bit = Precise_locs.inject_location_bits loc_bit in
+          Precise_locs.make_precise_loc ploc_bit ~size
+      and extract loc =
+        loc >>-: get
+      in
+      extract_loc res |> fst |> Response.map_join' extract join |> convert
+
   let as_location res =
     match A.Loc.get Main_locations.PLoc.key with
     | None ->
@@ -461,22 +507,6 @@ struct
     | LValue r -> Response.is_bottom r
     | Value r -> Response.is_bottom r
     | Address (r, _lval) -> Response.is_bottom r
-
-  (* Dependencies *)
-
-  let compute_deps eval_deps arg req =
-    let error = function
-      | Bottom -> Locations.Zone.bottom
-      | Top | DisabledDomain -> Locations.Zone.top
-    in
-    let compute cvalue =
-      eval_deps (cvalue, Locals_scoping.bottom ()) arg
-    in
-    req |> get_cvalue_model |> Result.fold ~error ~ok:compute
-
-  let lval_deps = compute_deps Register.eval_deps_lval
-  let expr_deps = compute_deps Register.eval_deps
-  let address_deps = compute_deps Register.eval_deps_addr
 end
 
 
@@ -512,21 +542,6 @@ let print_states ?filter req =
   E.print_states ?filter req
 
 
-(* Depedencies *)
-
-let expr_deps exp req =
-  let module E = Make () in
-  E.expr_deps exp req
-
-let lval_deps lval req =
-  let module E = Make () in
-  E.lval_deps lval req
-
-let address_deps lval req =
-  let module E = Make () in
-  E.address_deps lval req
-
-
 (* Evaluation *)
 
 module type Lvaluation =
@@ -647,10 +662,26 @@ let as_int evaluation =
   with Z.Overflow ->
     Result.error Top
 
-let as_location (Address lvaluation) =
+let as_precise_loc_result (Address lvaluation) =
+  let module E = (val lvaluation : Lvaluation) in
+  E.as_precise_loc E.v
+
+let as_precise_loc address =
+  match as_precise_loc_result address with
+  | Ok ploc -> ploc
+  | Error Bottom -> Precise_locs.loc_bottom
+  | Error (Top | DisabledDomain) -> Precise_locs.loc_top
+
+let as_location_result (Address lvaluation) =
   let module E = (val lvaluation : Lvaluation) in
   E.as_location E.v
 
+let as_location address =
+  match as_location_result address with
+  | Ok loc -> loc
+  | Error Bottom -> Locations.loc_bottom
+  | Error (Top | DisabledDomain) -> Locations.loc_top
+
 let as_zone_result (Address lvaluation) =
   let module E = (val lvaluation : Lvaluation) in
   E.as_zone E.v
@@ -669,10 +700,7 @@ let is_singleton: type a. a evaluation -> bool = function
     Cvalue.V.cardinal_zero_or_one cvalue && not (Cvalue.V.is_bottom cvalue)
   | Address _ as lvaluation ->
     let loc = as_location lvaluation in
-    let is_singleton loc =
-      Locations.cardinal_zero_or_one loc && not (Locations.is_bottom_loc loc)
-    in
-    Result.fold ~ok:is_singleton ~error:(fun _ -> false) loc
+    Locations.cardinal_zero_or_one loc && not (Locations.is_bottom_loc loc)
 
 let is_initialized (Value evaluation) =
   let module E = (val evaluation : Evaluation) in
@@ -687,6 +715,29 @@ let alarms : type a. a evaluation -> Alarms.t list =
     let module L = (val lvaluation : Lvaluation) in
     L.alarms L.v
 
+(* Dependencies *)
+
+let expr_deps expr request =
+  let lval_to_loc lv = eval_address lv request |> as_precise_loc in
+  Eva_utils.zone_of_expr lval_to_loc expr
+
+let lval_deps lval request =
+  let lval_to_loc lv = eval_address lv request |> as_precise_loc in
+  Eva_utils.zone_of_expr lval_to_loc (Cil.dummy_exp (Lval lval))
+
+let address_deps lval request =
+  let lval_to_loc lv = eval_address lv request |> as_precise_loc in
+  Eva_utils.indirect_zone_of_lval lval_to_loc lval
+
+type deps = Function_Froms.Deps.deps = {
+  data: Locations.Zone.t;
+  indirect: Locations.Zone.t;
+}
+
+let expr_dependencies expr request =
+  let lval_to_loc lv = eval_address lv request |> as_precise_loc in
+  Eva_utils.deps_of_expr lval_to_loc expr
+
 (* Reachability *)
 
 let is_empty rq =
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index e18f41a032527bbde86a2c4b4122423e202afb9d..ec7bc51d785b9b4c67436b2af5f527584a4412d6 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -61,7 +61,7 @@
       function body: all requests in the function will lead to a Bottom error.
     - results have not been saved, due to the [-eva-no-results] parameter:
       all requests in the function will lead to a Top error. *)
-val are_available: Cil_types.kernel_function -> bool
+val are_available : Cil_types.kernel_function -> bool
 
 type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
 
@@ -117,6 +117,11 @@ val after : Cil_types.stmt -> request
 (** Just before a statement or at the start of the analysis. *)
 val before_kinstr : Cil_types.kinstr -> request
 
+(** Evaluation in a given cvalue state. Callstacks selection are silently
+    ignored on such requests. For internal use, could be modified or removed
+    in a future version. *)
+val in_cvalue_state : Cvalue.Model.t -> request
+
 
 (** Callstack selection *)
 
@@ -165,7 +170,7 @@ val get_cvalue_model_result : request -> Cvalue.Model.t result
     request. If [filter] is provided, states are filtered on the given bases
     (for domains that support this feature).
     Returns a list of pair (name, state) for all available domains. *)
-val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
+val print_states : ?filter:Base.Hptset.t -> request -> (string * string) list
 
 (** Dependencies *)
 
@@ -181,6 +186,17 @@ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
     evaluate the given lvalue, excluding the lvalue zone itself. *)
 val address_deps : Cil_types.lval -> request -> Locations.Zone.t
 
+(** Memory dependencies of an expression. *)
+type deps = Function_Froms.Deps.deps = {
+  data: Locations.Zone.t;
+  (** Memory zone directly required to evaluate the given expression. *)
+  indirect: Locations.Zone.t;
+  (** Memory zone read to compute data addresses. *)
+}
+
+(** Computes (an overapproximation of) the memory dependencies of an
+    expression. *)
+val expr_dependencies : Cil_types.exp -> request -> deps
 
 (** Evaluation *)
 
@@ -243,16 +259,28 @@ val as_cvalue_result : value evaluation -> Cvalue.V.t result
 val as_cvalue_or_uninitialized : value evaluation -> Cvalue.V_Or_Uninitialized.t
 
 
+(** Converts into a C location abstraction. Error cases are converted into
+    bottom or top locations accordingly. *)
+val as_location : address evaluation -> Locations.location
+
 (** Converts into a C location abstraction. *)
-val as_location : address evaluation -> Locations.location result
+val as_location_result : address evaluation -> Locations.location result
 
 (** Converts into a Zone. Error cases are converted into bottom or top zones
     accordingly. *)
-val as_zone: address evaluation -> Locations.Zone.t
+val as_zone : address evaluation -> Locations.Zone.t
 
 (** Converts into a Zone result. *)
 val as_zone_result : address evaluation -> Locations.Zone.t result
 
+(** Converts into a C location abstraction. Error cases are converted into
+    bottom or top locations accordingly. *)
+val as_precise_loc : address evaluation -> Precise_locs.precise_location
+
+(** Converts into a C location abstraction. *)
+val as_precise_loc_result :
+  address evaluation -> Precise_locs.precise_location result
+
 
 (** Evaluation properties *)
 
@@ -288,7 +316,7 @@ val is_reachable : Cil_types.stmt -> bool
     the main function has been analyzed for [Kglobal]. *)
 val is_reachable_kinstr : Cil_types.kinstr -> bool
 
-val condition_truth_value: Cil_types.stmt -> bool * bool
+val condition_truth_value : Cil_types.stmt -> bool * bool
 (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
     (resp. snd) is true if and only if the condition of the 'if' has been
     evaluated to true (resp. false) at least once during the analysis. *)
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index f1119b1bed4377aa39a0f9a4b5cc69552238a4de..41a49e2e0a289dd89aa561ba2584d8fb2bc09b5c 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -44,7 +44,7 @@ let merge_call_froms table callsite froms =
 (** State for the analysis of one function call *)
 type from_state = {
   current_function: Kernel_function.t (** Function being analyzed *);
-  value_initial_state: Db.Value.state (** State of Value at the beginning of
+  value_initial_state: Cvalue.Model.t (** State of Eva at the beginning of
                                           the call *);
   table_for_calls: Function_Froms.t Kinstr.Hashtbl.t
 (** State of the From plugin for each statement containing a function call
@@ -94,7 +94,7 @@ let call_for_individual_froms callstack _kf call_type value_initial_state =
       register_from result
     | `Builtin None ->
       let behaviors =
-        !Db.Value.valid_behaviors current_function value_initial_state
+        Eva.Logic_inout.valid_behaviors current_function value_initial_state
       in
       compute_from_behaviors behaviors
     | `Spec spec ->
@@ -136,9 +136,10 @@ let compute_call_from_value_states current_function states =
       try Kinstr.Hashtbl.find table_for_calls (Cil_types.Kstmt callsite)
       with Not_found -> raise From_compute.Call_did_not_take_place
 
-    let get_value_state s =
-      try Stmt.Hashtbl.find states s
-      with Not_found -> Cvalue.Model.bottom
+    let stmt_request stmt =
+      Eva.Results.in_cvalue_state
+        (try Stmt.Hashtbl.find states stmt
+         with Not_found -> Cvalue.Model.bottom)
 
     let keep_base kf base =
       let fundec = Kernel_function.get_definition kf in
@@ -165,7 +166,7 @@ let record_for_individual_froms callstack cur_kf value_res =
           | { value_initial_state } :: _ -> value_initial_state
         in
         if From_parameters.VerifyAssigns.get () then
-          !Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
+          Eva.Logic_inout.verify_assigns cur_kf ~pre:pre_state froms;
         MemExec.replace memexec_counter froms;
         froms
 
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 9a53f5d988a5505a7a857d8bc1061685a8f38f6c..76b7fa9c5d6a08bcc0c6ca452460187c0e9ca830 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -31,42 +31,11 @@ exception Call_did_not_take_place
 module type To_Use =
 sig
   val get_from_call : kernel_function -> stmt -> Function_Froms.t
-  val get_value_state : stmt -> Db.Value.state
+  val stmt_request : stmt -> Eva.Results.request
   val keep_base : kernel_function -> Base.t -> bool
   val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
 end
 
-let rec find_deps_no_transitivity state expr =
-  (* The value of the expression [expr], just before executing the statement
-     [instr], is a function of the values of the returned zones. *)
-  match expr.enode with
-  | AlignOfE _| AlignOf _| SizeOfStr _ |SizeOfE _| SizeOf _ | Const _
-    -> Function_Froms.Deps.bottom
-  | AddrOf lv  | StartOf lv ->
-    let deps, _ = !Db.Value.lval_to_loc_with_deps_state (* loc ignored *)
-        state
-        ~deps:Zone.bottom
-        lv
-    in
-    Function_Froms.Deps.from_data_deps deps
-  | CastE (_, e)|UnOp (_, e, _) ->
-    find_deps_no_transitivity state e
-  | BinOp (_, e1, e2, _) ->
-    Function_Froms.Deps.join
-      (find_deps_no_transitivity state e1)
-      (find_deps_no_transitivity state e2)
-  | Lval v ->
-    find_deps_lval_no_transitivity state v
-
-and find_deps_lval_no_transitivity state lv =
-  let ind_deps, direct_deps, _exact =
-    !Db.Value.lval_to_zone_with_deps_state
-      state ~for_writing:false ~deps:(Some Zone.bottom) lv
-  in
-  From_parameters.debug "find_deps_lval_no_trs:@\n deps:%a@\n direct_deps:%a"
-    Zone.pretty ind_deps Zone.pretty direct_deps;
-  { Function_Froms.Deps.data = direct_deps; indirect = ind_deps }
-
 let compute_using_prototype_for_state state kf assigns =
   let varinfo = Kernel_function.get_vi kf in
   let return_deps,deps =
@@ -80,7 +49,7 @@ let compute_using_prototype_for_state state kf assigns =
       let (rt_typ,_,_,_) = splitFunctionTypeVI varinfo in
       let input_zone out ins =
         (* Technically out is unused, but there is a signature problem *)
-        !Db.Value.assigns_inputs_to_zone state (Writes [out, ins])
+        Eva.Logic_inout.assigns_inputs_to_zone state (Writes [out, ins])
       in
       let treat_assign acc (out, ins) =
         try
@@ -245,23 +214,21 @@ struct
 
 
   let find stmt deps_tbl expr =
-    let state = To_Use.get_value_state stmt in
-    let pre_trans = find_deps_no_transitivity state expr in
+    let request = To_Use.stmt_request stmt in
+    let pre_trans = Eva.Results.expr_dependencies expr request in
     merge_deps
       (fun d -> Function_Froms.Memory.find_precise deps_tbl d) pre_trans
 
-  let lval_to_zone_with_deps stmt ~for_writing lv =
-    let state = To_Use.get_value_state stmt in
-    !Db.Value.lval_to_zone_with_deps_state
-      state ~deps:(Some Zone.bottom) ~for_writing lv
+  let lval_to_zone_with_deps stmt lv =
+    let request = To_Use.stmt_request stmt in
+    Eva.Results.lval_deps lv request
 
   let lval_to_precise_loc_with_deps stmt ~for_writing lv =
-    let state = To_Use.get_value_state stmt in
-    let deps, loc =
-      !Db.Value.lval_to_precise_loc_with_deps_state
-        state ~deps:(Some Zone.bottom) lv
-    in
-    let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing loc in
+    let request = To_Use.stmt_request stmt in
+    let deps = Eva.Results.address_deps lv request in
+    let address = Eva.Results.eval_address ~for_writing lv request in
+    let loc = Eva.Results.as_precise_loc address
+    and exact = Eva.Results.(is_singleton address || is_bottom address) in
     deps, loc, exact
 
   let empty_from =
@@ -353,11 +320,9 @@ struct
 
     let transfer_call stmt dest f args _loc state =
       Db.yield ();
-      let value_state = To_Use.get_value_state stmt in
-      let f_deps, called_vinfos =
-        !Db.Value.expr_to_kernel_function_state
-          value_state ~deps:(Some Zone.bottom) f
-      in
+      let request = To_Use.stmt_request stmt in
+      let called_vinfos = Eva.Results.(eval_callee f request |> default []) in
+      let f_deps = Eva.Results.expr_deps f request in
       (* dependencies for the evaluation of [f] *)
       let f_deps =
         Function_Froms.Memory.find state.deps_table f_deps
@@ -428,7 +393,7 @@ struct
               let init = Cil.is_mutable_or_initialized lv in
               transfer_assign stmt ~init lv deps_ret state
       in
-      let f f acc =
+      let f acc f =
         let p = do_on f in
         match acc with
         | None -> Some p
@@ -441,7 +406,7 @@ struct
       in
       let result =
         try
-          (match Kernel_function.Hptset.fold f called_vinfos None with
+          (match List.fold_left f None called_vinfos with
            | None -> state
            | Some s -> s);
         with Call_did_not_take_place -> state
@@ -495,8 +460,8 @@ struct
 
 
     let transfer_guard s e d =
-      let value_state = To_Use.get_value_state s in
-      let interpreted_e = !Db.Value.eval_expr value_state e in
+      let request = To_Use.stmt_request s in
+      let interpreted_e = Eva.Results.(eval_exp e request |> as_cvalue) in
       let t1 = unrollType (typeOf e) in
       let do_then, do_else =
         if isIntegralType t1 || isPointerType t1
@@ -582,11 +547,8 @@ struct
     let deps_return =
       (match return.skind with
        | Return (Some ({enode = Lval v}),_) ->
-         let deps, target, _exact =
-           lval_to_zone_with_deps ~for_writing:false return v
-         in
-         let z = Zone.join target deps in
-         let deps = Function_Froms.Memory.find_precise state.deps_table z in
+         let zone = lval_to_zone_with_deps return v in
+         let deps = Function_Froms.Memory.find_precise state.deps_table zone in
          let size = Bit_utils.sizeof (Cil.typeOfLval v) in
          Function_Froms.(Memory.add_to_return ~size deps)
        | Return (None,_) ->
@@ -607,17 +569,7 @@ struct
       if not (Eva.Analysis.save_results kf) then Function_Froms.top
       else
         try
-          Stack.iter
-            (fun g ->
-               if kf == g then begin
-                 if Db.Value.ignored_recursive_call kf then
-                   From_parameters.error
-                     "during dependencies computations for %a, \
-                      ignoring probable recursive"
-                     Kernel_function.pretty kf;
-                 raise Exit
-               end)
-            call_stack;
+          Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
           Stack.push kf call_stack;
           let state =
             { empty_from with
@@ -671,8 +623,8 @@ struct
             deps_table = Function_Froms.Memory.empty }
 
   let compute_using_prototype kf =
-    let state = Db.Value.get_initial_state kf in
-    let behaviors = !Db.Value.valid_behaviors kf state in
+    let state = Eva.Results.(at_start_of kf |> get_cvalue_model) in
+    let behaviors = Eva.Logic_inout.valid_behaviors kf state in
     let assigns = Ast_info.merge_assigns behaviors in
     compute_using_prototype_for_state state kf assigns
 
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index b1017c26489bec197e63d2acd77ffdc687858fcf..e53256d9f9a1cf43ca0b5aefa5c42c5b36f8a72a 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -32,8 +32,9 @@ sig
   (** How to find the Froms for a given call during the analysis. *)
   val get_from_call : kernel_function -> stmt -> Function_Froms.t
 
-  (** How to find the state of Value at a given statement during the analysis.*)
-  val get_value_state : stmt -> Db.Value.state
+  (** The Eva request that can be used to evaluate expressions at a given
+      statement through the Eva public API. *)
+  val stmt_request : stmt -> Eva.Results.request
 
   val keep_base : kernel_function -> Base.t -> bool
   (** Return true if the given base is in scope after a call to the given
@@ -48,20 +49,12 @@ end
 (** Function that compute the Froms from a given prototype, called
     in the given state *)
 val compute_using_prototype_for_state :
-  Db.Value.state ->
+  Cvalue.Model.t ->
   Kernel_function.t ->
   assigns ->
   Function_Froms.froms
 
 
-(** Direct computation of the dependencies on expressions, offsets and
-    lvals. The state at the statement is taken from Values_To_Use *)
-val find_deps_no_transitivity :
-  Db.Value.state -> exp -> Function_Froms.Deps.t
-val find_deps_lval_no_transitivity :
-  Db.Value.state -> lval -> Function_Froms.Deps.t
-
-
 (** Functor computing the functional dependencies, according to the three
     modules above. *)
 module Make (To_Use: To_Use) : sig
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index a4f0a3e3065f582eab966749d0c87bcdb2265d98..fed913033aa883471918032861ca60a8ab72715a 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -37,7 +37,7 @@ let () = From_parameters.ForceDeps.set_output_dependencies [Tbl.self]
 let force_compute = ref (fun _ -> assert false)
 
 module To_Use = struct
-  let get_value_state s = Db.Value.get_stmt_state s
+  let stmt_request stmt = Eva.Results.before stmt
 
   let memo kf =
     Tbl.memo
@@ -110,16 +110,12 @@ let () =
        let deps = To_Use.memo v in
        Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt deps);
   Db.From.find_deps_no_transitivity :=
-    (fun stmt lv ->
-       let state = Db.Value.get_stmt_state stmt in
-       let deps = From_compute.find_deps_no_transitivity state lv in
-       Function_Froms.Deps.to_zone deps);
+    (fun stmt expr ->
+       Eva.Results.(before stmt |> expr_deps expr));
   (* Once this function has been moved to Eva, remove the dependency of Inout
      from From. *)
   Db.From.find_deps_no_transitivity_state :=
-    (fun s e ->
-       let deps = From_compute.find_deps_no_transitivity s e in
-       Function_Froms.Deps.to_zone deps);
+    (fun s e -> Eva.Results.(in_cvalue_state s |> expr_deps e));
 
   ignore (
     Db.register_compute "From.compute_all"
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index 5381137ce69085bf124554bfc4163c28d2f5b422..de32985952533de3805d69a9ea26e5d78aa4be34 100644
--- a/src/plugins/inout/cumulative_analysis.ml
+++ b/src/plugins/inout/cumulative_analysis.ml
@@ -37,27 +37,13 @@ let fold_implicit_initializer typ =
 
 let specialize_state_on_call ?stmt kf =
   match stmt with
-  | Some ({ skind = Instr (Call (_, _, l, _)) } as stmt) ->
-    let at_stmt = Db.Value.get_stmt_state stmt in
-    if Cvalue.Model.is_top at_stmt then
-      Cvalue.Model.top (* can occur with -no-results-function option *)
-    else !Db.Value.add_formals_to_state at_stmt kf l
-  | Some
-      ({skind =
-          Instr(Local_init(v, ConsInit(_,args,kind),_))} as stmt) ->
-    let at_stmt = Db.Value.get_stmt_state stmt in
-    if Cvalue.Model.is_top at_stmt then
-      Cvalue.Model.top
-    else begin
-      let args =
-        match kind with
-        | Constructor -> Cil.mkAddrOfVi v :: args
-        | Plain_func -> args
-      in
-      !Db.Value.add_formals_to_state at_stmt kf args
-    end
-  | _ -> Db.Value.get_initial_state kf
-
+  | None -> Eva.Results.(at_start_of kf |> get_cvalue_model)
+  | Some stmt ->
+    let filter = function
+      | (_, Kstmt s) :: _ -> Cil_datatype.Stmt.equal s stmt
+      | _ -> false
+    in
+    Eva.Results.(at_start_of kf |> filter_callstack filter |> get_cvalue_model)
 
 class virtual ['a] cumulative_visitor = object
   inherit frama_c_inplace as self
@@ -118,10 +104,6 @@ struct
     method private compute_kf_with_def kf =
       let f = Kernel_function.get_definition kf in
       if List.exists (Kernel_function.equal kf) call_stack then (
-        if Db.Value.ignored_recursive_call kf then
-          Inout_parameters.warning ~current:true ~once:true
-            "During %s analysis of %a: ignoring probable recursive call."
-            X.analysis_name Kernel_function.pretty kf;
         self#add_cycle (Kernel_function.Hptset.singleton kf);
         self#bottom
       )
diff --git a/src/plugins/inout/cumulative_analysis.mli b/src/plugins/inout/cumulative_analysis.mli
index f98bd1b9848ee3c045654c636598f4beab594b8c..a72397c8aa99ec62c04e37ce6f127f88dc8d7418 100644
--- a/src/plugins/inout/cumulative_analysis.mli
+++ b/src/plugins/inout/cumulative_analysis.mli
@@ -37,7 +37,7 @@ open Cil_types
 val fold_implicit_initializer: typ -> bool
 
 
-val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Db.Value.state
+val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Cvalue.Model.t
 (** If the given statement is a call to the given function,
     enrich the superposed memory state at this statement with
     the formal arguments of this function. This is usually more precise
@@ -50,7 +50,7 @@ val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Db.Value.state
 class virtual ['a] cumulative_visitor : object
   inherit Visitor.frama_c_inplace
 
-  method specialize_state_on_call: kernel_function -> Db.Value.state
+  method specialize_state_on_call: kernel_function -> Cvalue.Model.t
   (** If the current statement is a call to the given function,
       enrich the superposed memory state at this statement with
       the formal arguments of this function. Useful to do an analysis
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index f7436ea3a5cff07e7c188885d51aa35577aaa93d..bac263872419b63a3e26f35ab677dd4a83055be4 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -40,10 +40,8 @@ class virtual do_it_ = object(self)
     begin match base with
       | Var _ -> ()
       | Mem e ->
-        let state =
-          Db.Value.get_state (Kstmt (Option.get self#current_stmt))
-        in
-        let r = !Db.Value.eval_expr state e in
+        let stmt = Option.get self#current_stmt in
+        let r = Eva.Results.(before stmt |> eval_exp e |> as_cvalue) in
         let loc = loc_bytes_to_loc_bits r in
         let size = Bit_utils.sizeof_lval lv in
         self#join
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index 19e2f96f13057e9e06ac2444d9a85fcfcab95baa..c9787b60363db83ed5243c704e1b9f6ff33bea81 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -45,55 +45,43 @@ class virtual do_it_ = object(self)
       Cil.SkipChildren (* do not visit the additional lvals *)
     | _ -> super#vstmt_aux s
 
+  (* On assignment and addrof, only read the lvalue address.  *)
+  method private read_address lv =
+    let request = Eva.Results.before_kinstr self#current_kinstr in
+    let deps = Eva.Results.address_deps lv request in
+    self#join deps
+
   method! vlval lv =
-    let state = Db.Value.get_state self#current_kinstr in
-    let deps, bits_loc, _exact =
-      !Db.Value.lval_to_zone_with_deps_state
-        state ~deps:(Some Zone.bottom) ~for_writing:false lv
-    in
+    let request = Eva.Results.before_kinstr self#current_kinstr in
+    let deps = Eva.Results.lval_deps lv request in
     self#join deps;
-    self#join bits_loc;
     Cil.SkipChildren
 
-  method private do_assign lv =
-    let deps,_loc =
-      !Db.Value.lval_to_loc_with_deps (* loc ignored *)
-        ~deps:Zone.bottom
-        self#current_kinstr
-        lv
-    in
-    (*      Format.printf "do_assign deps:%a@."
-            Zone.pretty deps; *)
+  method private do_arg_calls stmt f args =
+    let deps = Eva.Results.(before stmt |> expr_deps f) in
     self#join deps;
-
-  method private do_arg_calls f args =
-    let state = Db.Value.get_state self#current_kinstr in
-    (if Cvalue.Model.is_top state then
-       self#join Zone.top
-     else
-       let deps_callees, callees =
-         !Db.Value.expr_to_kernel_function_state
-           ~deps:(Some Zone.bottom) state f
-       in
-       self#join deps_callees;
-       Kernel_function.Hptset.iter
-         (fun kf -> self#join (self#compute_kf kf)) callees;
-    );
-    List.iter
-      (fun exp -> ignore (visitFramacExpr (self:>frama_c_visitor) exp)) args
+    let () =
+      match Eva.Results.(before stmt |> eval_callee f) with
+      | Ok callees ->
+        List.iter (fun kf -> self#join (self#compute_kf kf)) callees
+      | Error (Top | DisabledDomain) -> self#join Zone.top;
+      | Error Bottom -> ()
+    in
+    List.iter (fun e -> ignore (visitFramacExpr (self:>frama_c_visitor) e)) args;
 
   method! vinst i =
-    if Db.Value.is_reachable (Db.Value.get_state self#current_kinstr) then begin
+    let stmt = Option.get self#current_stmt in
+    if Eva.Results.is_reachable stmt then begin
       match i with
       | Set (lv,exp,_) ->
-        self#do_assign lv;
+        self#read_address lv;
         ignore (visitFramacExpr (self:>frama_c_visitor) exp);
         Cil.SkipChildren
 
       | Local_init(v, AssignInit i,_) ->
         let rec aux lv = function
           | SingleInit e ->
-            self#do_assign lv;
+            self#read_address lv;
             ignore (visitFramacExpr (self:>frama_c_visitor) e)
           | CompoundInit (ct,initl) ->
             (* No need to consider implicit zero-initializers, for which
@@ -109,15 +97,15 @@ class virtual do_it_ = object(self)
         Cil.SkipChildren
 
       | Call (lv_opt,exp,args,_) ->
-        Option.iter self#do_assign lv_opt;
-        self#do_arg_calls exp args;
+        Option.iter self#read_address lv_opt;
+        self#do_arg_calls stmt exp args;
         Cil.SkipChildren
       | Local_init(v, ConsInit(f, args, Plain_func), _) ->
-        self#do_assign (Cil.var v);
-        self#do_arg_calls (Cil.evar f) args;
+        self#read_address (Cil.var v);
+        self#do_arg_calls stmt (Cil.evar f) args;
         Cil.SkipChildren
       | Local_init(v, ConsInit(f, args, Constructor), _) ->
-        self#do_arg_calls (Cil.evar f) (Cil.mkAddrOfVi v :: args);
+        self#do_arg_calls stmt (Cil.evar f) (Cil.mkAddrOfVi v :: args);
         Cil.SkipChildren
       | Skip _ | Asm _ | Code_annot _ -> Cil.DoChildren
     end
@@ -126,12 +114,7 @@ class virtual do_it_ = object(self)
   method! vexpr exp =
     match exp.enode with
     | AddrOf lv | StartOf lv ->
-      let deps,_loc =
-        !Db.Value.lval_to_loc_with_deps (* loc ignored *)
-          ~deps:Zone.bottom
-          self#current_kinstr lv
-      in
-      self#join deps;
+      self#read_address lv;
       Cil.SkipChildren
     | SizeOfE _ | AlignOfE _ | SizeOf _ | AlignOf _ ->
       (* we're not evaluating an expression here: there's no input. *)
@@ -140,9 +123,9 @@ class virtual do_it_ = object(self)
 
   method compute_funspec kf =
     let state = self#specialize_state_on_call kf in
-    let behaviors = !Db.Value.valid_behaviors kf state in
+    let behaviors = Eva.Logic_inout.valid_behaviors kf state in
     let assigns = Ast_info.merge_assigns behaviors in
-    !Db.Value.assigns_inputs_to_zone state assigns
+    Eva.Logic_inout.assigns_inputs_to_zone state assigns
 
   method clean_kf_result (_ : kernel_function) (r: Locations.Zone.t) = r
 end
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index adddc088f623ecfedc193549263e561afeb335df..4e5041fc2fd00a15e9b6b265ba1d49571a28a87e 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -191,7 +191,7 @@ let eval_assigns kf state assigns =
     }
 
 let compute_using_prototype_state state kf =
-  let behaviors = !Db.Value.valid_behaviors kf state in
+  let behaviors = Eva.Logic_inout.valid_behaviors kf state in
   let assigns = Ast_info.merge_assigns behaviors in
   eval_assigns kf state assigns
 
@@ -230,8 +230,9 @@ module CallwiseResults =
 module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
     val _version: string (* Debug: Callwise or functionwise *)
     val _kf: kernel_function (* Debug: Function being analyzed *)
-    val kf_pre_state: Db.Value.state (* Memory pre-state of the function. *)
-    val stmt_state: stmt -> Db.Value.state (* Memory state at the given stmt *)
+    val kf_pre_state: Cvalue.Model.t (* Memory pre-state of the function. *)
+    val stmt_state: stmt -> Cvalue.Model.t (* Memory state at the given stmt *)
+    val stmt_request: stmt -> Eva.Results.request (* Request at the given stmt *)
     val at_call: stmt -> kernel_function -> Inout_type.t (* Results of the
                                                             analysis for the given call. Must not contain locals or formals *)
   end) = struct
@@ -289,8 +290,8 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
 
   (* Transfer function on expression. *)
   let transfer_exp s exp data =
-    let state = X.stmt_state s in
-    let inputs = !Db.From.find_deps_no_transitivity_state state exp in
+    let request = X.stmt_request s in
+    let inputs = Eva.Results.expr_deps exp request in
     let new_inputs = Zone.diff inputs data.under_outputs_d in
     store_non_terminating_inputs new_inputs;
     {data with over_inputs_d = Zone.join data.over_inputs_d new_inputs}
@@ -298,12 +299,13 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
   (* Initialized const variables should be included as outputs of the function,
      so [for_writing] must be false for local initializations. It should be
      true for all other instructions. *)
-  let add_out ~for_writing state lv deps data =
-    let deps, new_outs, exact =
-      !Db.Value.lval_to_zone_with_deps_state state
-        ~deps:(Some deps) ~for_writing lv
-    in
+  let add_out ~for_writing request lv deps data =
+    let lv_address = Eva.Results.eval_address ~for_writing lv request in
+    let new_outs = Eva.Results.as_zone lv_address in
+    let exact = Eva.Results.is_singleton lv_address in
     store_non_terminating_outputs new_outs;
+    let lv_deps = Eva.Results.address_deps lv request in
+    let deps = Zone.join lv_deps deps in
     let new_inputs = Zone.diff deps data.under_outputs_d in
     store_non_terminating_inputs new_inputs;
     let new_sure_outs =
@@ -318,34 +320,21 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
       over_outputs_d = Zone.join data.over_outputs_d new_outs }
 
   let transfer_call ~for_writing s dest f args _loc data =
-    let state = X.stmt_state s in
-    let f_inputs, called =
-      !Db.Value.expr_to_kernel_function_state
-        ~deps:(Some Zone.bottom)
-        state
-        f
-    in
-    let acc_f_arg_inputs =
-      (* add the inputs of [argl] to the inputs of the
-         function expression *)
-      List.fold_right
-        (fun arg inputs ->
-           let arg_inputs = !Db.From.find_deps_no_transitivity_state
-               state arg
-           in Zone.join inputs arg_inputs)
-        args
-        f_inputs
-    in
+    let request = X.stmt_request s in
+    (* Join the inputs of [args] and of the function expression. *)
+    let eval_deps acc e = Zone.join acc (Eva.Results.expr_deps e request) in
+    let f_args_inputs = List.fold_left eval_deps Zone.bottom (f :: args) in
     let data =
       catenate
         data
-        { over_inputs_d = acc_f_arg_inputs ;
+        { over_inputs_d = f_args_inputs ;
           under_outputs_d = Zone.bottom;
           over_outputs_d = Zone.bottom; }
     in
+    let called = Eva.Results.(eval_callee f request |> default []) in
     let for_functions =
-      Kernel_function.Hptset.fold
-        (fun kf acc  ->
+      List.fold_left
+        (fun acc kf ->
            let res = X.at_call s kf in
            store_non_terminating_subcall data.over_outputs_d res;
            let for_function = {
@@ -354,15 +343,15 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
              over_outputs_d = res.over_outputs_if_termination;
            } in
            join for_function acc)
-        called
         bottom
+        called
     in
     let result = catenate data for_functions in
     let result =
       (* Treatment for the possible assignment of the call result *)
       (match dest with
        | None -> result
-       | Some lv -> add_out ~for_writing state lv Zone.bottom result)
+       | Some lv -> add_out ~for_writing request lv Zone.bottom result)
     in result
 
   (* Propagate all zones in predicates for the given statement, only in the case
@@ -378,7 +367,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
              let pre = X.kf_pre_state
              and here = X.stmt_state stmt in
              let deps =
-               Eva.Eval_terms.annot_predicate_deps ~pre ~here p.tp_statement
+               Eva.Logic_inout.predicate_deps ~pre ~here p.tp_statement
              in
              match deps with
              | None ->
@@ -395,18 +384,16 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
   let transfer_instr stmt (i: instr) (data: t) =
     match i with
     | Set (lv, exp, _) ->
-      let state = X.stmt_state stmt in
-      let e_inputs =
-        !Db.From.find_deps_no_transitivity_state state exp
-      in
-      add_out ~for_writing:true state lv e_inputs data
+      let request = X.stmt_request stmt in
+      let e_inputs = Eva.Results.expr_deps exp request in
+      add_out ~for_writing:true request lv e_inputs data
     | Local_init (v, AssignInit i, _) ->
-      let state = X.stmt_state stmt in
+      let request = X.stmt_request stmt in
       let rec aux lv i acc =
         match i with
         | SingleInit e ->
-          let e_inputs = !Db.From.find_deps_no_transitivity_state state e in
-          add_out ~for_writing:false state lv e_inputs acc
+          let e_inputs = Eva.Results.expr_deps e request in
+          add_out ~for_writing:false request lv e_inputs acc
         | CompoundInit(ct, initl) ->
           (* Avoid folding implicit zero-initializer of large arrays. *)
           let implicit = Cumulative_analysis.fold_implicit_initializer ct in
@@ -417,7 +404,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
                zone of the array as outputs. It is exactly the written zone for
                arrays of scalar elements. Nothing is read by zero-initializers,
                so the inputs are empty. *)
-            add_out ~for_writing:false state lv Zone.bottom acc
+            add_out ~for_writing:false request lv Zone.bottom acc
       in
       aux (Cil.var v) i data
     | Call (lvaloption,funcexp,argl,loc) ->
@@ -433,8 +420,8 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
      the condition. In this case, we just make sure that dead
      edges get bottom, instead of the input state. *)
   let transfer_guard stmt e t =
-    let state = X.stmt_state stmt in
-    let v_e = !Db.Value.eval_expr state e in
+    let request = X.stmt_request stmt in
+    let v_e = Eva.Results.(eval_exp e request |> as_cvalue) in
     let t1 = Cil.unrollType (Cil.typeOf e) in
     let do_then, do_else =
       if Cil.isIntegralType t1 || Cil.isPointerType t1
@@ -473,7 +460,7 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
   ;;
 
   let transfer_stmt s data =
-    if Db.Value.is_reachable (X.stmt_state s)
+    if Cvalue.Model.is_reachable (X.stmt_state s)
     then begin
       transfer_annotations s;
       transfer_stmt s data
@@ -663,20 +650,15 @@ module Callwise = struct
 
         (* Returns the [kf] pre-state with respect to the single [call_stack]. *)
         let kf_pre_state =
-          match Db.Value.get_initial_state_callstack kf with
-          | None ->
-            Cvalue.Model.bottom
-          | Some cs ->
-            begin
-              match Value_types.Callstack.Hashtbl.find_opt cs call_stack with
-              | None -> Cvalue.Model.bottom
-              | Some state -> state
-            end
+          Eva.Results.(at_start_of kf |> in_callstack call_stack |>
+                       get_cvalue_model)
 
         let stmt_state stmt =
           try Cil_datatype.Stmt.Hashtbl.find states stmt
           with Not_found -> Cvalue.Model.bottom
 
+        let stmt_request stmt = Eva.Results.in_cvalue_state (stmt_state stmt)
+
         let at_call stmt kf =
           let _cur_kf, table = List.hd !call_inout_stack in
           try
@@ -739,20 +721,12 @@ module FunctionWise = struct
       let module Computer = Computer(Fenv)(struct
           let _version = "functionwise"
           let _kf = kf
-          let kf_pre_state = Db.Value.get_initial_state kf
-          let stmt_state s = Db.Value.get_stmt_state s
+          let kf_pre_state = Eva.Results.(at_start_of kf |> get_cvalue_model)
+          let stmt_state s = Eva.Results.(before s |> get_cvalue_model)
+          let stmt_request s = Eva.Results.before s
           let at_call stmt kf = get_external_aux ~stmt kf
         end) in
-      Stack.iter
-        (fun g -> if kf == g then begin
-             if Db.Value.ignored_recursive_call kf then
-               Inout_parameters.warning ~current:true
-                 "During inout context analysis of %a:@ \
-                  ignoring probable recursive call."
-                 Kernel_function.pretty kf;
-             raise Exit
-           end)
-        call_stack;
+      Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
       Stack.push kf call_stack;
 
       let module [@warning "-60"] Compute =
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 8eb9a5f31d3739f81e581703d80613bf1ad165c3..4d06b9f1a51accebc2e6c80502bc94b9cd04b7ac 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -55,35 +55,32 @@ class virtual do_it_ = object(self)
     self#join bits_loc
 
   method! vinst i =
-    if Db.Value.is_reachable (Db.Value.noassert_get_state self#current_kinstr)
+    let stmt = Option.get self#current_stmt in
+    if Eva.Results.is_reachable stmt
     then
       (* noassert needed for Eval.memoize. Not really satisfactory *)
       begin
+        let assign_lval lval =
+          let for_writing = not (Cil.is_mutable_or_initialized lval) in
+          self#do_assign ~for_writing lval
+        in
         match i with
         | Set (lv,_,_) ->
-          let for_writing = not (Cil.is_mutable_or_initialized lv) in
-          self#do_assign ~for_writing lv
-        | Call (lv_opt,exp,_,_) ->
-          (match lv_opt with None -> ()
-                           | Some lv ->
-                             let for_writing =
-                               not (Cil.is_mutable_or_initialized lv)
-                             in
-                             self#do_assign ~for_writing lv);
-          let state = Db.Value.get_state self#current_kinstr in
-          if Cvalue.Model.is_top state then
-            self#join Zone.top
-          else
-            let _, callees =
-              !Db.Value.expr_to_kernel_function_state ~deps:None state exp in
-            Kernel_function.Hptset.iter
-              (fun kf ->
-                 let { Inout_type.over_outputs = z } =
-                   Operational_inputs.get_external_aux
-                     ?stmt:self#current_stmt kf
-                 in
-                 self#join z
-              ) callees
+          assign_lval lv
+        | Call (lv_opt, exp, _, _) ->
+          begin
+            Option.iter assign_lval lv_opt;
+            let callees = Eva.Results.(before stmt |> eval_callee exp) in
+            match callees with
+            | Ok callees ->
+              let join_outputs kf =
+                let inout = Operational_inputs.get_external_aux ~stmt kf in
+                self#join inout.over_outputs
+              in
+              List.iter join_outputs callees
+            | Error (Top | DisabledDomain) -> self#join Zone.top
+            | Error Bottom -> ()
+          end
         | Local_init (v, AssignInit i, _) ->
           let rec aux lv = function
             | SingleInit _ -> self#do_assign ~for_writing:false lv
@@ -102,8 +99,8 @@ class virtual do_it_ = object(self)
           in
           aux (Cil.var v) i
         | Local_init (v, ConsInit(f, _, _),_) ->
-          let state = Db.Value.get_state self#current_kinstr in
-          if Cvalue.Model.is_top state then self#join Zone.top
+          if Cvalue.Model.is_top Eva.Results.(before stmt |> get_cvalue_model)
+          then self#join Zone.top
           else begin
             let { Inout_type.over_outputs = z }  =
               Operational_inputs.get_external_aux ?stmt:self#current_stmt
@@ -125,9 +122,9 @@ class virtual do_it_ = object(self)
 
   method compute_funspec kf =
     let state = self#specialize_state_on_call kf in
-    let behaviors = !Db.Value.valid_behaviors kf state in
+    let behaviors = Eva.Logic_inout.valid_behaviors kf state in
     let assigns = Ast_info.merge_assigns behaviors in
-    !Db.Value.assigns_outputs_to_zone state ~result:None assigns
+    Eva.Logic_inout.assigns_outputs_to_zone state ~result:None assigns
 end
 
 module Analysis = Cumulative_analysis.Make(
diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml
index 3e8e1949b554ab1301184e93ff07527e95226348..f65fd3ad50b1eacea9334a306dbb95556b3ce873 100644
--- a/src/plugins/inout/register.ml
+++ b/src/plugins/inout/register.ml
@@ -52,7 +52,7 @@ let main () =
     Eva.Analysis.compute ();
     Callgraph.Uses.iter_in_rev_order
       (fun kf ->
-         if Kernel_function.is_definition kf && !Db.Value.is_called kf
+         if Kernel_function.is_definition kf && Eva.Results.is_called kf
          then begin
            if forceout
            then Inout_parameters.result "%a" Outputs.pretty_internal kf ;
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 571263696fd43639f7b508b5d6aef3f0785c5230..cab823fbddcd551f41fab6cf076920875f52eb13 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -613,8 +613,8 @@ let get_prop_scope_at_stmt kf stmt annot =
    in Db *)
 let emitter = lazy (
   let conv = List.map Typed_parameter.get in
-  let correctness = conv (Emitter.correctness_parameters !Db.Value.emitter) in
-  let tuning = conv (Emitter.tuning_parameters !Db.Value.emitter) in
+  let correctness = conv (Emitter.correctness_parameters Eva.Analysis.emitter) in
+  let tuning = conv (Emitter.tuning_parameters Eva.Analysis.emitter) in
   Emitter.create "RedundantAlarms" [Emitter.Property_status]
     ~correctness ~tuning)
 
diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle
index 6ed0132a710e40aab81aa419fcb7112775c3bd6d..f38325d385ce30bb9abc3f2cd2bd42a6c0c70f0b 100644
--- a/tests/builtins/oracle/alloc_weak.res.oracle
+++ b/tests/builtins/oracle/alloc_weak.res.oracle
@@ -950,7 +950,7 @@
 [inout] Out (internal) for function copy:
     dst; src; p
 [inout] Inputs for function copy:
-    t[0..1]
+    t{[0][bits 8 to 31]; [1][bits 0 to 23]}
 [inout] Out (internal) for function main1:
     __fc_heap_status; t[0..1]; i; p; n; r; __malloc_w_main1_l23[0..31]
 [inout] Inputs for function main1:
diff --git a/tests/value/oracle/loopfun.0.res.oracle b/tests/value/oracle/loopfun.0.res.oracle
index 97c9961dd442c52071b8ff9970b8a723eea6c82e..8e1dec0f58e0e08156ff46b0b588f4890010e2a9 100644
--- a/tests/value/oracle/loopfun.0.res.oracle
+++ b/tests/value/oracle/loopfun.0.res.oracle
@@ -62,4 +62,4 @@
 [inout] Out (internal) for function main:
     ANYTHING(origin:Unknown)
 [inout] Inputs for function main:
-    ANYTHING(origin:Unknown)
+    a
diff --git a/tests/value/oracle_equality/struct2.res.oracle b/tests/value/oracle_equality/struct2.res.oracle
index 31007513f85ece3f32c1295e5fbaad5985d2f497..d5f2dc058788e00396db9f2785b3850fd728239c 100644
--- a/tests/value/oracle_equality/struct2.res.oracle
+++ b/tests/value/oracle_equality/struct2.res.oracle
@@ -23,13 +23,19 @@
 ---
 >   tab6[0] ∈ {0}
 >       [1] ∈ {2}
-206,207c204,205
+186d183
+<   tab4[0] FROM tab2[0..1]; v; i (and SELF)
+188c185
+<   tab6[0..1] FROM tab2[0..1]; i; j (and SELF)
+---
+>   tab6[1] FROM tab2[0..1]; i; j
+206,207c203,204
 <     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
 <     tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
 ---
 >     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
 >     p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
-211c209
+211c208
 <            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
 ---
 >            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_multidim/struct2.res.oracle b/tests/value/oracle_multidim/struct2.res.oracle
index b18f3b3d19117c87628a5cbdae0c2a47a4ef0dbe..21073b5edf6801987743535a0b2e1e0bdd50df4e 100644
--- a/tests/value/oracle_multidim/struct2.res.oracle
+++ b/tests/value/oracle_multidim/struct2.res.oracle
@@ -4,7 +4,9 @@
 136,137d137
 <   tab4[0] ∈ {0; 2}
 <       [1] ∈ {0}
-206c206
+186d185
+<   tab4[0] FROM tab2[0..1]; v; i (and SELF)
+206c205
 <     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
 ---
 >     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0];
diff --git a/tests/value/oracle_octagon/relations2.res.oracle b/tests/value/oracle_octagon/relations2.res.oracle
index b44c30a0ec77a00cc1055343fa2223c1f5e69d03..a250063ee008db59cb92ba3ce23ff4eb5bfd0ad8 100644
--- a/tests/value/oracle_octagon/relations2.res.oracle
+++ b/tests/value/oracle_octagon/relations2.res.oracle
@@ -30,3 +30,15 @@
 <   len ∈ [--..--]
 ---
 >   len ∈ [0..1023]
+182c179
+<   \result FROM a[0..513]
+---
+>   \result FROM a[0..511]
+198c195
+<     a[0..513]
+---
+>     a[0..511]
+202c199
+<     sv; a[0..513]; T[0..6]
+---
+>     sv; a[0..511]; T[0..6]
diff --git a/tests/value/oracle_symblocs/struct2.res.oracle b/tests/value/oracle_symblocs/struct2.res.oracle
index 31bd4583d89f311ca047261d631ffb3fdaed779c..6a03454be556c668f58455fbd9873eb2149b864a 100644
--- a/tests/value/oracle_symblocs/struct2.res.oracle
+++ b/tests/value/oracle_symblocs/struct2.res.oracle
@@ -19,13 +19,19 @@
 ---
 >   tab6[0] ∈ {0}
 >       [1] ∈ {2}
-206,207c200,201
+186d179
+<   tab4[0] FROM tab2[0..1]; v; i (and SELF)
+188c181
+<   tab6[0..1] FROM tab2[0..1]; i; j (and SELF)
+---
+>   tab6[1] FROM tab2[0..1]; i; j
+206,207c199,200
 <     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
 <     tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
 ---
 >     s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
 >     p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
-211c205
+211c204
 <            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
 ---
 >            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];