From 64264c615e08bea7beaf662c632e63b272d26e76 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 7 Feb 2022 16:57:30 +0100
Subject: [PATCH] [Reduc] Use the new Eva API
---
src/plugins/reduc/hyp.ml | 3 +--
src/plugins/reduc/value2acsl.ml | 14 ++++++--------
src/plugins/reduc/value2acsl.mli | 4 ++--
3 files changed, 9 insertions(+), 12 deletions(-)
diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
index fc4fabf2763..882e9a63c23 100644
--- a/src/plugins/reduc/hyp.ml
+++ b/src/plugins/reduc/hyp.ml
@@ -36,12 +36,11 @@ class hypotheses_visitor (env: Collect.env) = object(self)
method! vstmt_aux stmt =
let kf = Option.get (self#current_kf) in
- let state = Db.Value.get_stmt_state stmt in
if Collect.should_annotate_stmt env stmt then begin
let vars = Collect.get_relevant_vars_stmt env kf stmt in
List.iter
(fun e ->
- let p_opt = pred_opt_from_expr_state state e in
+ let p_opt = pred_opt_from_expr_state stmt e in
Option.iter (Misc.assert_and_validate ~kf stmt) p_opt)
vars
end;
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
index c91d1ba6992..e5201a791cc 100644
--- a/src/plugins/reduc/value2acsl.ml
+++ b/src/plugins/reduc/value2acsl.ml
@@ -165,15 +165,13 @@ let value_to_predicate_opt ?(loc=Location.unknown) t v =
with
| Not_based_on_null -> (* base_offsets_to_predicate ~loc t m *) None
-let exp_to_predicate ?(loc=Location.unknown) state e =
- let value = !Db.Value.eval_expr ~with_alarms:CilE.warn_none_mode state e in
+let exp_to_predicate ?(loc=Location.unknown) stmt e =
+ let value = Eva.Results.(before stmt |> eval_exp e |> as_ival) in
let te = Logic_utils.expr_to_term ~coerce:false e in
- value_to_predicate_opt ~loc te value
+ Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
-let lval_to_predicate ?(loc=Location.unknown) state lv =
- let value = snd(!Db.Value.eval_lval
- ~with_alarms:CilE.warn_none_mode None state lv)
- in
+let lval_to_predicate ?(loc=Location.unknown) stmt lv =
+ let value = Eva.Results.(before stmt |> eval_lval lv |> as_ival) in
let e = Cil.new_exp ~loc (Lval lv) in
let te = Logic_utils.expr_to_term ~coerce:false e in
- value_to_predicate_opt ~loc te value
+ Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli
index 17546299c21..4d1aacea7b0 100644
--- a/src/plugins/reduc/value2acsl.mli
+++ b/src/plugins/reduc/value2acsl.mli
@@ -27,5 +27,5 @@ open Cil_types
@return None if no such predicate can be created. *)
val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option
-val lval_to_predicate: ?loc:location -> Cvalue.Model.t -> lval -> predicate option
-val exp_to_predicate: ?loc:location -> Cvalue.Model.t -> exp -> predicate option
+val lval_to_predicate: ?loc:location -> Cil_types.stmt -> lval -> predicate option
+val exp_to_predicate: ?loc:location -> Cil_types.stmt -> exp -> predicate option
--
GitLab