[Eva] Uses the evaluation engine on Cvalue instead of Db.Value.

src/plugins/eva/domains/cvalue/builtins_misc.ml

@@ -22,6 +22,7 @@
 
 open Eva_utils
 
+open Lattice_bounds.Bottom.Operators
 
 let frama_C_assert state actuals =
   let do_bottom () =
@@ -35,10 +36,14 @@ let frama_C_assert state actuals =
       then do_bottom ()
       else if Cvalue.V.contains_zero arg
       then begin
-        let state = !Db.Value.reduce_by_cond state arg_exp true in
-        if Cvalue.Model.is_reachable state
-        then (warning_once_current "Frama_C_assert: unknown"; state)
-        else do_bottom ()
+        let state =
+          let* valuation = fst (Cvalue_queries.reduce state arg_exp true) in
+          let valuation = Cvalue_queries.to_domain_valuation valuation in
+          Cvalue_transfer.update valuation state
+        in
+        match state with
+        | `Value state -> warning_once_current "Frama_C_assert: unknown"; state
+        | `Bottom -> do_bottom ()
       end
       else begin
         warning_once_current "Frama_C_assert: true";

src/plugins/eva/domains/cvalue/builtins_split.ml

@@ -74,7 +74,7 @@ let warning warn s =
    [max_card] elements. *)
 let split_v ~warn lv state max_card =
   if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
-    let loc = !Db.Value.lval_to_loc_state state lv in
+    let loc = Cvalue_queries.lval_to_loc state lv in
     if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
       let v_indet = Cvalue.Model.find_indeterminate state loc in
       let v = Cvalue.V_Or_Uninitialized.get_v v_indet in

src/plugins/eva/utils/widen.ml

@@ -499,7 +499,7 @@ module Parsed_Dynamic_Hints =
 let dynamic_bases_of_lval states e offset =
   let lv = (Mem e, offset) in
   List.fold_left (fun acc' state ->
-      let location = !Db.Value.lval_to_loc_state state lv in
+      let location = Cvalue_queries.lval_to_loc state lv in
       Locations.Location_Bits.fold_bases
         (fun base acc'' -> Base.Hptset.add base acc'')
         location.Locations.loc acc'