From e3d5e4579cd2ba2570499ce3f17c85164f84c62b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Jul 2022 09:47:29 +0200
Subject: [PATCH] [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 | 10 ++++++++++
src/plugins/eva/dune | 2 +-
src/plugins/eva/legacy/logic_inout.ml | 6 ++----
src/plugins/eva/legacy/logic_inout.mli | 10 +++++++++-
src/plugins/eva/register.ml | 2 ++
5 files changed, 24 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 1c07614bd1a..1d48b8bd770 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 502fec6d6ed..6a91dd3bcb3 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 aebbdbd39bc..64edb349ce7 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 7af69cb1ef9..f29202c96c7 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 e48168230e4..d216a3abb25 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
--
GitLab