diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 1c07614bd1a1376f87fc6b08ca8d95b5495baf8f..1d48b8bd770c42905f1018e69de78a5447f7e547 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -608,6 +608,16 @@ module Cvalue_callbacks: sig
 
 end
 
+module Logic_inout: sig
+
+  (** 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 Eval_terms: sig
 
   (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 502fec6d6edf50ebae146a7f34a37b63502fcad6..6a91dd3bcb3cc98108b020c1331916c90dcefc62 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 legacy/eval_terms.mli utils/eva_results.mli
   utils/unit_tests.mli)
  (action (run %{deps})))
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index aebbdbd39bcbf3bd9e84a94dc30a53652b3deaf3..64edb349ce73906c2350ffd7a664064ea8fc099d 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -176,7 +176,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 +186,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/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 7af69cb1ef9e1fab669041eca3639b4cb9f3ba3c..f29202c96c739e9ae8d939674510a52ddfbb0425 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -20,4 +20,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** No function exported. Registers Db.Value.verify_assigns_from. *)
+[@@@ api_start]
+
+(** 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..d216a3abb25084c1526df8258b1ead0cdf93e73e 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -505,6 +505,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