diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 3b5ca67cc99adcad579cd980791dea983595a2b8..67cf369519044ca31cb4dc91f82d9c235522529b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1637,7 +1637,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
add_node ~min ~max:abs_max new_reml m v new_offr subr
;;
- let update_itv_with_rem ~exact ~offset ~abs_max ~size ~rem v curr_off tree =
+ let update_itv_with_rem ~exact ~once ~offset ~abs_max ~size ~rem v curr_off tree =
if Int.(equal size zero) then curr_off, tree else
let off1, t1 = keep_above ~offset:abs_max curr_off tree in
let off2, t2 = keep_below ~offset curr_off tree in
@@ -1659,9 +1659,16 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let new_offset = Integer.max offset impz.offset in
let rem = realign ~offset ~new_offset rem size in
let r_node = realign ~offset:impz.offset ~new_offset r_node m_node in
+ let node_abs_max = impz.offset +~ max in
+ let end_reached, write_max =
+ if node_abs_max >=~ abs_max
+ then true, abs_max
+ else false, node_abs_max
+ in
let new_r, new_m, new_v =
let joined_value = V.join v_node v in
- if v_is_isotropic || (Rel.equal rem r_node && m_node =~ size)
+ if (v_is_isotropic && (once || size >~ (write_max -~ new_offset)))
+ || (Rel.equal rem r_node && m_node =~ size)
then r_node, m_node, V.anisotropic_cast ~size:m_node joined_value
else if V.is_isotropic v_node
then rem, size, V.anisotropic_cast ~size joined_value
@@ -1671,12 +1678,6 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let new_rem = Rel.zero and new_modu = Integer.one in
new_rem, new_modu, new_value
in
- let node_abs_max = impz.offset +~ max in
- let end_reached, write_max =
- if node_abs_max >=~ abs_max
- then true, abs_max
- else false, node_abs_max
- in
let new_left_offset, new_left_tree =
add_node
~min:new_offset ~max:write_max
@@ -1690,7 +1691,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
union !left_offset !left_tree off1 t1
;;
- let update_itv = update_itv_with_rem ~rem:Rel.zero;;
+ let update_itv = update_itv_with_rem ~rem:Rel.zero ~once:false
(* This should be in Int_Intervals, but is currently needed here.
Returns an interval with reversed bounds when the intersection is empty. *)
@@ -1988,7 +1989,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let update = update_itv_with_rem ~exact in
let treat_interval (imin, imax) (v, modu, rem) acc =
let dmin, dmax = imin +~ start_dest, imax +~ start_dest in
- snd (update
+ snd (update ~once:true
~offset:dmin ~abs_max:dmax ~rem:rem ~size:modu v Integer.zero acc)
in
fold_between ~entire:false (Int.zero, stop) treat_interval from to_
@@ -2153,7 +2154,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
r
let add ?(exact=true) (min, max) (v, modu, rem) m =
- snd (update_itv_with_rem ~exact
+ snd (update_itv_with_rem ~exact ~once:true
~offset:min ~abs_max:max ~rem ~size:modu v Integer.zero m)
let find_imprecise ~validity m =
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index a6894e6df987f96c10c477928035b0d0138d7cbd..61a577a188d430f830604df840ed5ad6f1a0cbdd 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -129,6 +129,9 @@
{0},{12})) failed; destination is not exact
[eva:alarm] memset.c:107: Warning:
accessing uninitialized left-value. assert \initialized(&s->ptr);
+[eva:alarm] memset.c:109: Warning:
+ pointer comparison. assert \pointer_comparable((void *)q, (void *)0);
+[eva:alarm] memset.c:109: Warning: out of bounds write. assert \valid(q);
[eva] Recording results for memset_weak_base
[from] Computing for function memset_weak_base
[from] Done for function memset_weak_base
@@ -139,19 +142,26 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ memset.c:106: imprecise merge of addresses
+ (read in 3 statements, propagated through 1 statement)
+ garbled mix of &{x}
[eva] memset.c:85: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function memset_weak_base:
+ NULL[rbits 128 to 1927] ∈ [--..--]
__fc_heap_status ∈ [--..--]
x ∈ {42} or UNINITIALIZED
s ∈ {{ &__malloc_w_memset_weak_base_l101[0] }}
- q ∈ {{ NULL ; &x }}
- __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
+ q ∈ {{ NULL + [0..237] ; &x }}
+ __malloc_w_memset_weak_base_l101[0].i ∈ [--..--] or UNINITIALIZED
[0].c ∈ {0; 1} or UNINITIALIZED
[0].[bits 40 to 63] ∈
{0} or UNINITIALIZED
[0].ptr ∈
- {{ NULL ; &x }} or UNINITIALIZED
+ {{ garbled mix of &{x}
+ (origin: Merge {memset.c:106}) }} or UNINITIALIZED
[eva:final-states] Values at end of function test:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
@@ -214,8 +224,7 @@
x ∈ {{ (void *)&a }}
a ∈ {0}
[eva:final-states] Values at end of function main:
- NULL[rbits 128 to 143] ∈ {66} repeated %8
- [rbits 144 to 1927] ∈ [--..--]
+ NULL[rbits 128 to 1927] ∈ [--..--]
__fc_heap_status ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
@@ -266,12 +275,12 @@
[4]{.f3; .f4[0..2]} ∈ {-16843010; 0}
S_incomplete_type[bits 0 to 7] ∈ {65}
[bits 8 to ..] ∈ [--..--] or UNINITIALIZED
- __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
+ __malloc_w_memset_weak_base_l101[0].i ∈ [--..--] or UNINITIALIZED
[0].c ∈ {0; 1} or UNINITIALIZED
[0].[bits 40 to 63] ∈
{0} or UNINITIALIZED
[0].ptr ∈
- {0} or UNINITIALIZED or ESCAPINGADDR
+ [--..--] or UNINITIALIZED or ESCAPINGADDR
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to malloc at memset.c:101 (by memset_weak_base):
__fc_heap_status FROM __fc_heap_status; size (and SELF)
@@ -350,10 +359,16 @@
[from] call to uninit at memset.c:114 (by main):
NO EFFECTS
[from] call to memset_weak_base at memset.c:115 (by main):
+ NULL[16..240]
+ FROM __fc_heap_status;
+ __malloc_w_memset_weak_base_l101[0].ptr (and SELF)
__fc_heap_status FROM __fc_heap_status (and SELF)
__malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] entry point:
- NULL[16..17] FROM \nothing
+ NULL[16..17] FROM __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+ [18..240]
+ FROM __fc_heap_status;
+ __malloc_w_memset_weak_base_l101[0].ptr (and SELF)
__fc_heap_status FROM __fc_heap_status (and SELF)
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
@@ -374,7 +389,8 @@
__malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function memset_weak_base:
- __fc_heap_status; x; s; q; __malloc_w_memset_weak_base_l101[0]
+ NULL[16..240]; __fc_heap_status; x; s; q;
+ __malloc_w_memset_weak_base_l101[0]
[inout] Inputs for function memset_weak_base:
__fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
[inout] InOut (internal) for function memset_weak_base:
@@ -412,7 +428,7 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- NULL[16..17]; __fc_heap_status; t1[0..99]; t2[0..99]; t3[10..99];
+ NULL[16..240]; __fc_heap_status; t1[0..99]; t2[0..99]; t3[10..99];
t4[1..99]; t5[0..99]; t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99];
t10[4..12]; t11[2..6]; t12[0..96]; ts[0..4];
S_incomplete_type[bits 0 to 7]; __malloc_w_memset_weak_base_l101[0]
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index 8dd87df7eb7f3067eab8a7efd31c326edc5fa577..479f9ea51af0339ef2bb27d509311ae60c658dd8 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -64,7 +64,7 @@
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
@@ -126,7 +126,7 @@
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index e4a0ef1e213946250f153be76b9b034b3f23c643..d4033b4c6a51235d0b47922c0a7d5a863f79d709 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -47,21 +47,29 @@
Called from offsetmap.i:87.
[eva] using specification for function Frama_C_interval
[eva] Done for function Frama_C_interval
-[eva] offsetmap.i:90: Frama_C_show_each_1_256_257: {0; 257}
+[eva] offsetmap.i:90: Frama_C_show_each_1_256_257: [-2147483648..2147483647]
+[eva:alarm] offsetmap.i:95: Warning:
+ pointer comparison. assert \pointer_comparable((void *)q, (void *)0);
+[eva:alarm] offsetmap.i:95: Warning: out of bounds write. assert \valid(q);
[eva] computing for function Frama_C_interval <- h <- main.
Called from offsetmap.i:101.
[eva] Done for function Frama_C_interval
-[eva] offsetmap.i:104: Frama_C_show_each_1_256_257: {0; 257}
+[eva] offsetmap.i:104: Frama_C_show_each_1_256_257: [-32768..32767]
[eva] Recording results for h
[eva] Done for function h
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ offsetmap.i:94: imprecise merge of addresses
+ (read in 2 statements, propagated through 0 statements)
+ garbled mix of &{x}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
@@ -102,19 +110,19 @@
q ∈ {{ &s + [0..9999999] }}
c2 ∈ [0..8]
[eva:final-states] Values at end of function h:
- x ∈ [0..257]
+ x ∈ [--..--]
i_0 ∈ [0..6]
p_0 ∈ {{ &t + {1} }}
q ∈ {{ NULL ; &x }}
t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
- [bits 8 to 119]# ∈ {0; 257} repeated %16, bits 8 to 119
+ {[0][bits 8 to 15]; [1..6]; [7][bits 0 to 7]} ∈ [--..--]
[7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
sp ∈ {{ &t + [1..13],1%2 }}
[eva:final-states] Values at end of function main:
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
diff --git a/tests/value/oracle/offsetmap.2.res.oracle b/tests/value/oracle/offsetmap.2.res.oracle
index d39ab3e4cdf645e136bed345549fc01f687aeb85..33d782cf04bc117c1285caaed11cb7033a6038b6 100644
--- a/tests/value/oracle/offsetmap.2.res.oracle
+++ b/tests/value/oracle/offsetmap.2.res.oracle
@@ -64,7 +64,7 @@
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
@@ -127,7 +127,7 @@
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
[bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
- [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ {[2][bits 8 to 31]; [3..8]} ∈ [--..--]
[9] ∈ {0}
T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
[0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
diff --git a/tests/value/oracle/struct2.res.oracle b/tests/value/oracle/struct2.res.oracle
index ee8eebba63902d880f163f2993a3bbc322628e86..699931bbdf610dd68673359cec09c7c8fb8ae527 100644
--- a/tests/value/oracle/struct2.res.oracle
+++ b/tests/value/oracle/struct2.res.oracle
@@ -98,7 +98,8 @@
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f_precis:
- NULL[rbits 32768 to 32799] ∈ {{ NULL + [--..--] ; (? *)&a }}
+ NULL[rbits 32768 to 32799] ∈
+ {{ garbled mix of &{a} (origin: Merge {struct2.i:149}) }}
[rbits 32800 to 65543] ∈ [--..--]
tab_s[0] ∈ {0}
[1].a ∈ [--..--]
diff --git a/tests/value/oracle_apron/offsetmap.1.res.oracle b/tests/value/oracle_apron/offsetmap.1.res.oracle
index 5c1fbd1e023b397a94f273318f1a322e5e75241b..54a3c9f489329f9a6bf1d759101941258998c93a 100644
--- a/tests/value/oracle_apron/offsetmap.1.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.1.res.oracle
@@ -1,19 +1,19 @@
-77,78c77
+85,86c85
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-80,81c79
+88,89c87
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-130,131c128
+138,139c136
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-133,134c130
+141,142c138
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
diff --git a/tests/value/oracle_equality/struct2.res.oracle b/tests/value/oracle_equality/struct2.res.oracle
index d5f2dc058788e00396db9f2785b3850fd728239c..0ca131c45d53b75f4cbd5db19d04c8690893ce33 100644
--- a/tests/value/oracle_equality/struct2.res.oracle
+++ b/tests/value/oracle_equality/struct2.res.oracle
@@ -11,31 +11,31 @@
< [scope:rm_asserts] removing 2 assertion(s)
---
> [scope:rm_asserts] removing 1 assertion(s)
-135,137c133,134
+136,138c134,135
< tab3[0..1] ∈ [--..--]
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
---
> tab3[0] ∈ {0; 1}
> [1] ∈ [--..--]
-140c137,138
+141c138,139
< tab6[0..1] ∈ {0; 2}
---
> tab6[0] ∈ {0}
> [1] ∈ {2}
-186d183
+187d184
< tab4[0] FROM tab2[0..1]; v; i (and SELF)
-188c185
+189c186
< tab6[0..1] FROM tab2[0..1]; i; j (and SELF)
---
> tab6[1] FROM tab2[0..1]; i; j
-206,207c203,204
+207,208c204,205
< s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
< tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
---
> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
> p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
-211c208
+212c209
< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
---
> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_multidim/struct2.res.oracle b/tests/value/oracle_multidim/struct2.res.oracle
index 21073b5edf6801987743535a0b2e1e0bdd50df4e..f4e6b3fb65c13b3f6fd91fb6e2c4159633e32717 100644
--- a/tests/value/oracle_multidim/struct2.res.oracle
+++ b/tests/value/oracle_multidim/struct2.res.oracle
@@ -1,12 +1,12 @@
53a54,55
> [kernel] struct2.i:78: Warning:
> all target addresses were invalid. This path is assumed to be dead.
-136,137d137
+137,138d138
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
-186d185
+187d186
< tab4[0] FROM tab2[0..1]; v; i (and SELF)
-206c205
+207c206
< 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];
diff --git a/tests/value/oracle_symblocs/struct2.res.oracle b/tests/value/oracle_symblocs/struct2.res.oracle
index 6a03454be556c668f58455fbd9873eb2149b864a..c74386cdbefacf8dc061a50ba168044ba484e091 100644
--- a/tests/value/oracle_symblocs/struct2.res.oracle
+++ b/tests/value/oracle_symblocs/struct2.res.oracle
@@ -11,27 +11,27 @@
< [eva:alarm] struct2.i:185: Warning:
98d93
< [scope:rm_asserts] removing 2 assertion(s)
-136,137d130
+137,138d131
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
-140c133,134
+141c134,135
< tab6[0..1] ∈ {0; 2}
---
> tab6[0] ∈ {0}
> [1] ∈ {2}
-186d179
+187d180
< tab4[0] FROM tab2[0..1]; v; i (and SELF)
-188c181
+189c182
< tab6[0..1] FROM tab2[0..1]; i; j (and SELF)
---
> tab6[1] FROM tab2[0..1]; i; j
-206,207c199,200
+207,208c200,201
< s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
< tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
---
> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
> p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
-211c204
+212c205
< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
---
> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];