diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index a21577b15097c2a7897aa580cf72687b3c0f63de..85835a4966e9698c6afb0cbfd4cfb3df631d73f7 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -374,26 +374,18 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
| AAssert (_, p)
| AInvariant (_, true, p) ->
begin
- let env =
- Eva.Eval_terms.env_annot
- ~pre:X.kf_pre_state
- ~here:(X.stmt_state stmt)
- ()
+ 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
in
- match Eva.Eval_terms.predicate_deps env p.tp_statement with
+ match deps with
| None ->
(* To be sound, we should perform a join with the top zone here.
We do nothing instead because the latter behavior would
directly disable memexec. *)
()
- | Some logic_deps ->
- let p_zone =
- Cil_datatype.Logic_label.Map.fold
- (fun _ -> Zone.join)
- logic_deps
- Zone.bottom
- in
- store_non_terminating_logic_inputs p_zone
+ | Some p_zone -> store_non_terminating_logic_inputs p_zone
end
| _ -> ())
stmt
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 47c7fed9e7950bff77bb4acc941ee5d496f7850d..6c935365f412bd32d06873384effb8fd7ee8d376 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -268,20 +268,13 @@ module Value_parameters: sig
end
module Eval_terms: sig
- type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
-
- (** Evaluation environment. Currently available are function Pre and Post, or
- the environment to evaluate an annotation *)
- type eval_env
- val env_annot :
- ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
- unit -> eval_env
- (** Dependencies needed to evaluate a term or a predicate *)
- type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
- (** [predicate_deps env p] computes the logic dependencies needed to evaluate
- [p] in the given evaluation environment [env].
- @return None on either an evaluation error or on unsupported construct. *)
- val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
+ (** [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 Unit_tests: sig
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c36e84a45b30286e18f983451fdff6d6a4171a81..a75bfed0d139992f8f602c3218285215a1101720 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -2745,6 +2745,16 @@ 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/value/legacy/eval_terms.mli b/src/plugins/value/legacy/eval_terms.mli
index 59a798c9e55a97bfa3d31dd90b47da8a969ba592..cff8567815ab453e72462ac147747305a2604fb3 100644
--- a/src/plugins/value/legacy/eval_terms.mli
+++ b/src/plugins/value/legacy/eval_terms.mli
@@ -49,22 +49,18 @@ val pretty_logic_evaluation_error :
exception LogicEvalError of logic_evaluation_error
-[@@@ api_start]
type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
(** Evaluation environment. Currently available are function Pre and Post, or
- the environment to evaluate an annotation *)
+ the environment to evaluate an annotation. *)
type eval_env
-[@@@ api_end]
val make_env: Model.t Abstract_domain.logic_environment -> Model.t -> eval_env
val env_pre_f : pre:Model.t -> unit -> eval_env
-[@@@ api_start]
val env_annot :
?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
unit -> eval_env
-[@@@ api_end]
val env_post_f :
?c_labels:labels_states -> pre:Model.t -> post:Model.t ->
result:varinfo option -> unit -> eval_env
@@ -75,10 +71,8 @@ val env_only_here: Model.t -> eval_env
val env_current_state: eval_env -> Model.t
-[@@@ api_start]
(** Dependencies needed to evaluate a term or a predicate *)
type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-[@@@ api_end]
(** Three modes to handle the alarms when evaluating a logical term. *)
type alarm_mode =
@@ -117,12 +111,22 @@ val eval_tlval_as_zone :
val eval_predicate :
eval_env -> predicate -> predicate_status
-[@@@ api_start]
(** [predicate_deps env p] computes the logic dependencies needed to evaluate
[p] in the given evaluation environment [env].
- @return None on either an evaluation error or on unsupported construct. *)
+ Returns None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
-[@@@ api_end]
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]