Skip to content
Snippets Groups Projects
Commit f90aaaf3 authored by David Bühler's avatar David Bühler
Browse files

[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.
parent 28cfb4f2
No related branches found
No related tags found
No related merge requests found
...@@ -60,7 +60,7 @@ let update valuation t = ...@@ -60,7 +60,7 @@ let update valuation t =
let process exp record t = let process exp record t =
match exp.enode with match exp.enode with
| Lval lv -> | Lval lv ->
if record.reductness = Reduced if record.reductness = Reduced && Cil.isScalarType (Cil.typeOfLval lv)
then then
let {v; initialized; escaping} = record.value in let {v; initialized; escaping} = record.value in
let v = unbottomize v in let v = unbottomize v in
......
53a54,55 53a54,55
> [kernel] struct2.i:78: Warning: > [kernel] struct2.i:78: Warning:
> all target addresses were invalid. This path is assumed to be dead. > all target addresses were invalid. This path is assumed to be dead.
75a78,81 136,137d137
> [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
< tab4[0] ∈ {0; 2} < tab4[0] ∈ {0; 2}
< [1] ∈ {0} < [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]; tab4[0]; tab5[0];
--- ---
> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; > s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0];
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment