[Eva] Logic_inout: exports function [verify_assigns] in Eva.mli.

Used by the from plugin when option -from-verify-assigns is enabled.

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

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})))

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

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]

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