From 56ff49f945bdece8ec360f7f83a14a8cbfcf8717 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 31 Mar 2022 22:42:04 +0200
Subject: [PATCH] [Eva] multidim: improve precision when an expression is not
in the valuation
---
src/plugins/value/domains/multidim_domain.ml | 13 +++++++------
1 file changed, 7 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 2e81e5cf589..823572a226e 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -628,15 +628,16 @@ struct
(* Eva Transfer *)
- let make_oracle valuation : Cil_types.exp -> value = fun exp ->
+ let valuation_to_oracle state valuation : Cil_types.exp -> value = fun exp ->
+ let multidim_oracle = mk_oracle state in
match valuation.Abstract_domain.find exp with
- | `Top -> Value.top
+ | `Top -> multidim_oracle exp
| `Value {value={v=`Bottom}} -> Value.bottom
| `Value {value={v=`Value value}} -> value
let assume_exp valuation expr record state' =
state' >>- fun state ->
- let oracle = make_oracle valuation in
+ let oracle = valuation_to_oracle state valuation in
match expr.enode with
| Lval lv ->
let value = Value_or_Uninitialized.from_flagged record.value in
@@ -726,9 +727,9 @@ struct
overwrite ~oracle state dst src
let assign _kinstr left expr assigned_value valuation state =
+ let oracle = valuation_to_oracle state valuation in
let state = update_array_segmentation left.lval (Some expr) state in
assume_valuation valuation state >>-: fun state ->
- let oracle = make_oracle valuation in
assign_lval left.lval assigned_value oracle state
let assume _stmt _expr _pos valuation state =
@@ -739,7 +740,7 @@ struct
then
Self.abort ~current:true
"The multidim domain does not support recursive calls yet";
- let oracle = make_oracle valuation in
+ let oracle = valuation_to_oracle state valuation in
let bind state arg =
state >>-: assign_lval (Cil.var arg.formal) arg.avalue oracle
in
@@ -756,7 +757,7 @@ struct
let show_expr valuation state fmt expr =
match expr.enode with
| Lval lval | StartOf lval ->
- let oracle = make_oracle valuation in
+ let oracle = valuation_to_oracle state valuation in
begin match Location.of_lval oracle lval with
| `Top -> Format.fprintf fmt "%s" (Unicode.top_string ())
| `Value loc ->
--
GitLab