From d44331ff653aa250eb8dc2730c23543a5be89b78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 20:08:17 +0200
Subject: [PATCH] [Eva] Uses the evaluation engine on Cvalue instead of
Db.Value.
---
src/plugins/eva/domains/cvalue/builtins_misc.ml | 13 +++++++++----
src/plugins/eva/domains/cvalue/builtins_split.ml | 2 +-
src/plugins/eva/utils/widen.ml | 2 +-
3 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 93fbcf970dc..47d8da9c980 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/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";
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index 5d6721b188a..a6a2cf2812a 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/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
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 2e4564b4ef0..b26bb71371f 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/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'
--
GitLab