[Reduc] Use the new Eva API

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;

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)

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