From f90aaaf3e29feea078320c1d7c9c4f0583306129 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Apr 2022 15:17:18 +0200
Subject: [PATCH] [Eva] Cvalue domain: uses the valuation only for lvalues of
scalar type.
The cvalues cannot precisely represent structs and arrays: they are irrelevant
and could degrade the state precision for such lvalues.
---
.../value/domains/cvalue/cvalue_transfer.ml | 2 +-
tests/value/oracle_multidim/struct2.res.oracle | 14 ++------------
2 files changed, 3 insertions(+), 13 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index cf095c211eb..10b707287ea 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -60,7 +60,7 @@ let update valuation t =
let process exp record t =
match exp.enode with
| Lval lv ->
- if record.reductness = Reduced
+ if record.reductness = Reduced && Cil.isScalarType (Cil.typeOfLval lv)
then
let {v; initialized; escaping} = record.value in
let v = unbottomize v in
diff --git a/tests/value/oracle_multidim/struct2.res.oracle b/tests/value/oracle_multidim/struct2.res.oracle
index 8d07aa9bd96..b18f3b3d191 100644
--- a/tests/value/oracle_multidim/struct2.res.oracle
+++ b/tests/value/oracle_multidim/struct2.res.oracle
@@ -1,20 +1,10 @@
53a54,55
> [kernel] struct2.i:78: Warning:
> all target addresses were invalid. This path is assumed to be dead.
-75a78,81
-> [eva] struct2.i:173:
-> Assigning imprecise value to ((s1.c)->c)->b
-> (pointing to s2 with offsets {352}).
-> The imprecision originates from Misaligned Bottom
-129,130c135
-< s8.a ∈ {0}
-< .b ∈ {{ &a }}
----
-> s8 ∈ {{ garbled mix of &{a} (origin: Misaligned Bottom) }}
-136,137d140
+136,137d137
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
-206c209
+206c206
< s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
---
> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0];
--
GitLab