diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index dfe0c43c7dfc87df17a5c15b403739a53f44baa7..98c8fc246b5b29c385962602ccb0d469896b2020 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -610,6 +610,18 @@ end
module Logic_inout: sig
+ (** 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:
@@ -634,17 +646,6 @@ module Logic_inout: sig
end
-module Eval_terms: 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].
- 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
-end
-
module Eva_results: sig
type results
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 6a91dd3bcb3cc98108b020c1331916c90dcefc62..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/logic_inout.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/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/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 8d6cd7d02787c84b7086f9d726ad9d48d2118dbd..98803359c8570b7c958d8e5e455be5af70710e12 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -22,6 +22,17 @@
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 =
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index f26ba262e163603ad15adff669524b8d83fa91d4..92d6afd81687589a37b2bfbdcadea6bfe67a6cba 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -22,6 +22,18 @@
[@@@ 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:
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index adddc088f623ecfedc193549263e561afeb335df..20af7014d751d1abcfc4780d08d4db993d884515 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -378,7 +378,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 ->