From b217d637b1773318a069e59fb27911e00a93ca01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Jul 2022 10:31:48 +0200
Subject: [PATCH] [Eva] Moves exported function [predicate_deps] in
logic_inout.
---
src/plugins/eva/Eva.mli | 23 ++++++++++++-----------
src/plugins/eva/dune | 2 +-
src/plugins/eva/legacy/eval_terms.ml | 11 -----------
src/plugins/eva/legacy/eval_terms.mli | 13 -------------
src/plugins/eva/legacy/logic_inout.ml | 11 +++++++++++
src/plugins/eva/legacy/logic_inout.mli | 12 ++++++++++++
src/plugins/inout/operational_inputs.ml | 2 +-
7 files changed, 37 insertions(+), 37 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index dfe0c43c7df..98c8fc246b5 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 6a91dd3bcb3..771f0d370a7 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 ae229527a49..8c46196981a 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 95e826556e3..a8b326ffc3d 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 8d6cd7d0278..98803359c85 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 f26ba262e16..92d6afd8168 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 adddc088f62..20af7014d75 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 ->
--
GitLab