diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 3b5ca67cc99adcad579cd980791dea983595a2b8..a22454c830a9499e98f9ec8f2bad41e40e549c46 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1637,7 +1637,11 @@ 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 =
+ (* If [once] holds, interprets a single write from [offset] to [abs_max]
+ of the value [v] of size [size], repeated to fill the interval.
+ Otherwise, interprets independent writes of the value [v] of size [size]
+ at possible offsets, starting from [offset] until [abs_max]. *)
+ 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,24 +1663,40 @@ 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_node_size = write_max -~ new_offset 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)
- then r_node, m_node, V.anisotropic_cast ~size:m_node joined_value
+ (* If the write has the same size and alignment as the existing
+ node, then afterward each write location contains either the
+ previous node value or the written value. *)
+ if Rel.equal rem r_node && m_node =~ size
+ then rem, size, joined_value
+ (* Each write location contains either the written value, or bits
+ from the previous node value, which is a proper value if it is
+ isotropic. *)
else if V.is_isotropic v_node
then rem, size, V.anisotropic_cast ~size joined_value
+ (* If the new node is smaller than the write size, then either it
+ contains only the new value, or only the previous node value.
+ If the new value is isotropic, we can then reuse the alignment
+ and size of the existing node. *)
+ else if v_is_isotropic && (once || size >~ new_node_size)
+ then r_node, m_node, V.anisotropic_cast ~size:m_node joined_value
else
+ (* Otherwise, bits of the existing node value can be mixed with
+ the written value. We topify the joined value to be sound,
+ but this is imprecise. *)
let origin = Origin.(current Merge) in
let new_value = V.topify_with_origin origin joined_value in
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 +1710,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 +2008,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 +2173,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/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index f0c86e9e19d7f609b5eb98ddc2a6283a925be82d..30e1e75319187264ceb950e914869d8162f3fd13 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -174,14 +174,14 @@ let imprecise_copy ~name ~src_loc ~dst_loc ~dst_expr state =
return [bottom]. In this case, return the previously computed state *)
if Model.is_reachable new_state then new_state else state
-(* Creates the location {loc + [0..max_size-1]} of size char. *)
-let char_location loc max_size =
+(* Creates the location {loc + [min_size..max_size-1]} of size char. *)
+let char_location loc ?(min_size=Int.zero) max_size =
let size_char = Bit_utils.sizeofchar () in
let max = Int.sub max_size size_char in
(* Use ranges modulo char_bits to read and write byte-by-byte, which can
preserve some precision.*)
let shift =
- Ival.inject_interval ~min:(Some Int.zero) ~max:(Some max)
+ Ival.inject_interval ~min:(Some min_size) ~max:(Some max)
~rem:Int.zero ~modu:size_char
in
let loc = Location_Bits.shift shift loc in
@@ -271,45 +271,65 @@ let () =
(* Implementation of [memset] that accepts imprecise arguments. *)
let frama_c_memset_imprecise state dst_expr dst v size =
let size_min, size_max = min_max_size size in
+ let exact = Location_Bits.cardinal_zero_or_one dst in
+ (* Write [v] everywhere that is written, between [dst] and [dst+size_min]. *)
+ let state, min_zone =
+ if Int.gt size_min Int.zero then
+ let size = size_min in
+ let value = Cvalue.V_Or_Uninitialized.initialized v in
+ let from = Cvalue.V_Offsetmap.create ~size ~size_v:Integer.eight value in
+ warn_imprecise_offsm_write ~name:"memset" dst_expr from;
+ let state =
+ Cvalue.Model.paste_offsetmap ~from ~size ~exact ~dst_loc:dst state
+ in
+ let loc = make_loc dst (Int_Base.Value size_min) in
+ let written_zone = enumerate_valid_bits Locations.Write loc in
+ state, written_zone
+ else state, Zone.bottom
+ in
(* Write [v] everywhere that might be written, ie between
- [dst] and [dst+size-1]. *)
- let state, over_zone =
- if Int.gt size_max Int.zero then
- let loc = char_location dst size_max in
+ [dst+size_min] and [dst+size_max-1]. *)
+ let state, extra_zone =
+ if Int.gt size_max size_min then
+ let loc = char_location dst ~min_size:size_min size_max in
warn_imprecise_write ~name:"memset" dst_expr loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
let written_zone = enumerate_valid_bits Locations.Write loc in
state, written_zone
else state, Zone.bottom
in
- (* Write "sure" bytes in an exact way: they exist only if there is only
- one base, and within it, size_min+leftmost_loc > rightmost_loc *)
- let state, sure_zone =
- try
- let base, offset = Location_Bits.find_lonely_key dst in
- let minb, maxb = match Ival.min_and_max offset with
- | Some minb, Some maxb -> minb, maxb
- | _ -> raise Not_found
- in
- let sure = Int.sub (Int.add minb size_min) maxb in
- if Int.gt sure Int.zero then
- let dst_loc = Location_Bits.inject base (Ival.inject_singleton maxb) in
- let vuninit = V_Or_Uninitialized.initialized v in
- let size_v = Bit_utils.sizeofchar () in
- let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
- warn_imprecise_offsm_write ~name:"memset" dst_expr from;
- let state =
- Cvalue.Model.paste_offsetmap
- ~from ~dst_loc ~size:sure ~exact:true state
+ let over_zone = Zone.join min_zone extra_zone in
+ if exact
+ then state, min_zone, over_zone
+ else
+ (* Write "sure" bytes in an exact way: they exist only if there is only
+ one base, and within it, size_min+leftmost_loc > rightmost_loc *)
+ let state, sure_zone =
+ try
+ let base, offset = Location_Bits.find_lonely_key dst in
+ let minb, maxb = match Ival.min_and_max offset with
+ | Some minb, Some maxb -> minb, maxb
+ | _ -> raise Not_found
in
- let sure_loc = make_loc dst_loc (Int_Base.inject sure) in
- let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
- state, sure_zone
- else
- state, Zone.bottom
- with Not_found -> state, Zone.bottom (* from find_lonely_key + explicit raise *)
- in
- state, sure_zone, over_zone
+ let sure = Int.sub (Int.add minb size_min) maxb in
+ if Int.gt sure Int.zero then
+ let dst_loc = Location_Bits.inject base (Ival.inject_singleton maxb) in
+ let vuninit = V_Or_Uninitialized.initialized v in
+ let size_v = Bit_utils.sizeofchar () in
+ let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
+ warn_imprecise_offsm_write ~name:"memset" dst_expr from;
+ let state =
+ Cvalue.Model.paste_offsetmap
+ ~from ~dst_loc ~size:sure ~exact:true state
+ in
+ let sure_loc = make_loc dst_loc (Int_Base.inject sure) in
+ let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
+ state, sure_zone
+ else
+ state, Zone.bottom
+ with Not_found -> state, Zone.bottom (* from find_lonely_key + explicit raise *)
+ in
+ state, sure_zone, over_zone
(* Type that describes why the 'precise memset' builtin may fail. *)
type imprecise_memset_reason =
diff --git a/tests/builtins/memset.c b/tests/builtins/memset.c
index 9c537d24550636043bb34e9e7001e9820bcf01ea..0b42eac05f019b35c9753003d51400178b26e39d 100644
--- a/tests/builtins/memset.c
+++ b/tests/builtins/memset.c
@@ -3,7 +3,7 @@
*/
#include "string.h"
-
+#include "stdlib.h"
int t1[100];
int t2[100];
@@ -89,7 +89,28 @@ void uninit() {
memset(x, 0, 4);
}
+typedef struct S {
+ int i;
+ char c;
+ int *ptr;
+} st;
+
+void memset_weak_base () {
+ int x;
+ /*@ eva_allocate fresh_weak; */
+ st *s = malloc(sizeof(st));
+ if (s == NULL) return;
+ s->i = 421;
+ s->c = 1;
+ s->ptr = &x;
+ memset(s, 0, sizeof(st));
+ int *q = s->ptr; /* As the base is weak, s->ptr must be 0 or &x.
+ This should not be a garbled mix. */
+ if (q != NULL) *q = 42; // This write should be valid.
+}
+
void main() {
test();
uninit();
+ memset_weak_base();
}
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 81ad7400cbf0cce906879475122cb6216e196365..ce26d8999c1d6c35dc5ef450ac8a51382d3ca221 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -30,7 +30,7 @@
vol ∈ [--..--]
S_incomplete_type[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[eva] computing for function test <- main.
- Called from memset.c:93.
+ Called from memset.c:113.
[eva] memset.c:33: Call to builtin memset
[eva] memset.c:33: function memset: precondition 'valid_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:151:
@@ -107,7 +107,7 @@
[from] Done for function test
[eva] Done for function test
[eva] computing for function uninit <- main.
- Called from memset.c:94.
+ Called from memset.c:114.
[eva:alarm] memset.c:85: Warning:
accessing uninitialized left-value. assert \initialized(&x);
[eva:alarm] memset.c:89: Warning:
@@ -118,12 +118,40 @@
[from] Computing for function uninit
[from] Done for function uninit
[eva] Done for function uninit
+[eva] computing for function memset_weak_base <- main.
+ Called from memset.c:115.
+[eva] memset.c:101: Call to builtin malloc
+[eva] memset.c:101: allocating weak variable __malloc_w_memset_weak_base_l101
+[eva] memset.c:106: Call to builtin memset
+[eva] memset.c:106: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:106:
+ Call to builtin precise_memset(({{ (void *)&__malloc_w_memset_weak_base_l101 }},
+ {0},{12})) failed; destination is not exact
+[eva:alarm] memset.c:107: Warning:
+ accessing uninitialized left-value. assert \initialized(&s->ptr);
+[eva] Recording results for memset_weak_base
+[from] Computing for function memset_weak_base
+[from] Done for function memset_weak_base
+[eva] Done for function memset_weak_base
+[eva:locals-escaping] memset.c:115: Warning:
+ locals {x} escaping the scope of memset_weak_base through __malloc_w_memset_weak_base_l101
[eva] Recording results for main
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
[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:
+ __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
+ [0].c ∈ {0; 1} or UNINITIALIZED
+ [0].[bits 40 to 63] ∈
+ {0} or UNINITIALIZED
+ [0].ptr ∈
+ {{ NULL ; &x }} or UNINITIALIZED
[eva:final-states] Values at end of function test:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
@@ -152,7 +180,31 @@
[3]# ∈ {153} repeated %8
[4..6]# ∈ {0; 153} repeated %8
[7..99] ∈ {0}
- t12[0..96]# ∈ {0; 1} repeated %8
+ t12[0]# ∈ {0; 1} repeated %8
+ [1..7] ∈ {0}
+ [8]# ∈ {0; 1} repeated %8
+ [9..15] ∈ {0}
+ [16]# ∈ {0; 1} repeated %8
+ [17..23] ∈ {0}
+ [24]# ∈ {0; 1} repeated %8
+ [25..31] ∈ {0}
+ [32]# ∈ {0; 1} repeated %8
+ [33..39] ∈ {0}
+ [40]# ∈ {0; 1} repeated %8
+ [41..47] ∈ {0}
+ [48]# ∈ {0; 1} repeated %8
+ [49..55] ∈ {0}
+ [56]# ∈ {0; 1} repeated %8
+ [57..63] ∈ {0}
+ [64]# ∈ {0; 1} repeated %8
+ [65..71] ∈ {0}
+ [72]# ∈ {0; 1} repeated %8
+ [73..79] ∈ {0}
+ [80]# ∈ {0; 1} repeated %8
+ [81..87] ∈ {0}
+ [88]# ∈ {0; 1} repeated %8
+ [89..95] ∈ {0}
+ [96]# ∈ {0; 1} repeated %8
[97..99] ∈ {0}
ts[0].f1 ∈ {-2; 0}
[0].[bits 8 to 15] ∈ {0; 254}
@@ -188,6 +240,7 @@
[eva:final-states] Values at end of function main:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
+ __fc_heap_status ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
@@ -213,7 +266,31 @@
[3]# ∈ {153} repeated %8
[4..6]# ∈ {0; 153} repeated %8
[7..99] ∈ {0}
- t12[0..96]# ∈ {0; 1} repeated %8
+ t12[0]# ∈ {0; 1} repeated %8
+ [1..7] ∈ {0}
+ [8]# ∈ {0; 1} repeated %8
+ [9..15] ∈ {0}
+ [16]# ∈ {0; 1} repeated %8
+ [17..23] ∈ {0}
+ [24]# ∈ {0; 1} repeated %8
+ [25..31] ∈ {0}
+ [32]# ∈ {0; 1} repeated %8
+ [33..39] ∈ {0}
+ [40]# ∈ {0; 1} repeated %8
+ [41..47] ∈ {0}
+ [48]# ∈ {0; 1} repeated %8
+ [49..55] ∈ {0}
+ [56]# ∈ {0; 1} repeated %8
+ [57..63] ∈ {0}
+ [64]# ∈ {0; 1} repeated %8
+ [65..71] ∈ {0}
+ [72]# ∈ {0; 1} repeated %8
+ [73..79] ∈ {0}
+ [80]# ∈ {0; 1} repeated %8
+ [81..87] ∈ {0}
+ [88]# ∈ {0; 1} repeated %8
+ [89..95] ∈ {0}
+ [96]# ∈ {0; 1} repeated %8
[97..99] ∈ {0}
ts[0].f1 ∈ {-2; 0}
[0].[bits 8 to 15] ∈ {0; 254}
@@ -237,7 +314,19 @@
[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
+ [0].c ∈ {0; 1} or UNINITIALIZED
+ [0].[bits 40 to 63] ∈
+ {0} or UNINITIALIZED
+ [0].ptr ∈
+ {0} 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)
+ \result FROM __fc_heap_status; size
+[from] call to memset at memset.c:106 (by memset_weak_base):
+ __malloc_w_memset_weak_base_l101[0] FROM c (and SELF)
+ \result FROM s
[from] call to memset at memset.c:33 (by test):
t1[0..99] FROM c
\result FROM s
@@ -275,7 +364,9 @@
ts[0..4] FROM c
\result FROM s
[from] call to memset at memset.c:72 (by test):
- t12[0..96] FROM c (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM c (and SELF)
\result FROM s
[from] call to memset at memset.c:74 (by test):
\result FROM s
@@ -288,7 +379,7 @@
[from] call to memset at memset.c:89 (by uninit):
a FROM c
\result FROM s
-[from] call to test at memset.c:93 (by main):
+[from] call to test at memset.c:113 (by main):
NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
@@ -303,13 +394,19 @@
[7..12] FROM \nothing (and SELF)
t11{[2]; [4..6]} FROM \nothing (and SELF)
[3] FROM \nothing
- t12[0..96] FROM \nothing (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
-[from] call to uninit at memset.c:94 (by main):
+[from] call to uninit at memset.c:114 (by main):
NO EFFECTS
+[from] call to memset_weak_base at memset.c:115 (by main):
+ __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
+ __fc_heap_status FROM __fc_heap_status (and SELF)
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
@@ -323,14 +420,29 @@
[7..12] FROM \nothing (and SELF)
t11{[2]; [4..6]} FROM \nothing (and SELF)
[3] FROM \nothing
- t12[0..96] FROM \nothing (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
+ __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]
+[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:
+ Operational inputs:
+ __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+ Operational inputs on termination:
+ __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
+ Sure outputs:
+ s; q
[inout] Out (internal) for function test:
NULL[16..17]; 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]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}; ts[0..4]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
S_incomplete_type[bits 0 to 7]
[inout] Inputs for function test:
incomplete_type; vol
@@ -355,16 +467,22 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- NULL[16..17]; 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]
+ NULL[16..17]; __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]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}; ts[0..4]; S_incomplete_type[bits 0 to 7];
+ __malloc_w_memset_weak_base_l101[0]
[inout] Inputs for function main:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
[inout] InOut (internal) for function main:
Operational inputs:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
Operational inputs on termination:
- incomplete_type; vol
+ __fc_heap_status; incomplete_type; vol;
+ __malloc_w_memset_weak_base_l101[0].ptr
Sure outputs:
NULL[16..17]; t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6];
t11[3]; S_incomplete_type[bits 0 to 7]
diff --git a/tests/value/offsetmap.i b/tests/value/offsetmap.i
index 74db362fd49ad6a6cd11121d5436c5d022142585..9aab8c31905d8293c381c44385905599e2cd7f34 100644
--- a/tests/value/offsetmap.i
+++ b/tests/value/offsetmap.i
@@ -1,6 +1,6 @@
/* run.config*
-
- STDOPT: #""
+ STDOPT: #"-eva-ilevel 8"
+ STDOPT: #"-eva-ilevel 2"
STDOPT: #"-eva-warn-copy-indeterminate=-f,-g"
*/
@@ -70,8 +70,42 @@ void g(int i) {
char c2 = *q;
}
+/*@ assigns \result \from min, max;
+ ensures min <= \result <= max; */
+int Frama_C_interval(int min, int max);
+
+/* Test the soundness in offsetmaps when:
+ - writing an isotropic value [v] (all bits are 0, or all bits are 1);
+ - to an imprecise abstract location when all possible locations are
+ contiguous and non-overlapping;
+ - the number of possible locations is strictly greater than -eva-ilevel;
+ - the target location contains a value with a different size or alignment
+ than the write of [v]. */
+void h(void) {
+ int x = 257;
+ /* Writing one byte to 0 in 4-byte integer x. */
+ int i = Frama_C_interval(0, 3);
+ char *p = (char *)&x + i;
+ *p = 0;
+ Frama_C_show_each_1_256_257(x); // Must at least contain 1, 256 and 257.
+ /* Same operation on 4-byte pointer p. */
+ int *q = &x;
+ p = (char *)&q + i;
+ *p = 0; // q is now completely invalid and should be a garbled mix.
+ if (q != 0) *q = 42; // Thus there must be a memory access alarm here.
+ /* Unaligned write in an array. */
+ short t[8];
+ //@ loop unroll 8;
+ for (int j = 0; j < 8; j++) { t[j] = 257; }
+ p = (char *)t + 1;
+ i = Frama_C_interval(0, 6);
+ short *sp = (short *)p + i;
+ *sp = 0;
+ Frama_C_show_each_1_256_257(t[4]); // Must at least contain 1, 256 and 257.
+}
void main (int i) {
f();
g(i);
+ h();
}
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index 7172b2b74c34b9d561f5c2c1a2d13dad2115b86c..479f9ea51af0339ef2bb27d509311ae60c658dd8 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -24,7 +24,7 @@
a2 ∈ {0}
s[0..9999999] ∈ {0}
[eva] computing for function f <- main.
- Called from offsetmap.i:75.
+ Called from offsetmap.i:108.
[eva] offsetmap.i:19: starting to merge loop iterations
[eva] offsetmap.i:29: starting to merge loop iterations
[eva:alarm] offsetmap.i:51: Warning:
@@ -32,7 +32,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
- Called from offsetmap.i:76.
+ Called from offsetmap.i:109.
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert 0 ≤ i_0;
[eva:alarm] offsetmap.i:66: Warning:
@@ -41,6 +41,22 @@
[kernel] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ 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; 1; 256; 257}
+[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; 1; 256; 257}
+[eva] Recording results for h
+[eva] Done for function h
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -48,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
@@ -88,11 +104,29 @@
c1 ∈ {0; 7}
q ∈ {{ &s + [0..9999999] }}
c2 ∈ {0; 1; 3; 7; 8}
+[eva:final-states] Values at end of function h:
+ x[bits 0 to 7]# ∈ {0; 42; 257}%32, bits 0 to 7
+ [bits 8 to 15]# ∈ {0; 42; 257}%32, bits 8 to 15
+ [bits 16 to 23]# ∈ {0; 42; 257}%32, bits 16 to 23
+ [bits 24 to 31]# ∈ {0; 42; 257}%32, bits 24 to 31
+ i_0 ∈ {0; 1; 2; 3; 4; 5; 6}
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ [bits 8 to 23]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 24 to 39]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 40 to 55]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 56 to 71]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 72 to 87]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 88 to 103]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 104 to 119]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
+ sp ∈ {{ &t + {1; 3; 5; 7; 9; 11; 13} }}
[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
@@ -131,10 +165,16 @@
[from] Done for function f
[from] Computing for function g
[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ \result FROM min; max
[from] Function f:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -153,6 +193,8 @@
a2 FROM \nothing
[from] Function g:
s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
[from] Function main:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -181,6 +223,10 @@
s[0..9999999]; p_0; c1; q; c2
[inout] Inputs for function g:
s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
[inout] Out (internal) for function main:
TT{[0..8]; [9][bits 0 to 7]};
T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index 396fe80c6c408ba761c316248436c66cfc744a4f..d4033b4c6a51235d0b47922c0a7d5a863f79d709 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -24,7 +24,7 @@
a2 ∈ {0}
s[0..9999999] ∈ {0}
[eva] computing for function f <- main.
- Called from offsetmap.i:75.
+ Called from offsetmap.i:108.
[eva] offsetmap.i:19: starting to merge loop iterations
[eva] offsetmap.i:29: starting to merge loop iterations
[eva:alarm] offsetmap.i:51: Warning:
@@ -32,7 +32,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
- Called from offsetmap.i:76.
+ Called from offsetmap.i:109.
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert 0 ≤ i_0;
[eva:alarm] offsetmap.i:66: Warning:
@@ -41,14 +41,35 @@
[kernel] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ 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: [-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: [-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
@@ -63,8 +84,7 @@
i ∈ {9}
a[bits 0 to 7] ∈ {1; 6}
[bits 8 to 31]# ∈ {6}%32, bits 8 to 31
- b[bits 0 to 7] ∈ {0; 1}
- [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ b ∈ {0; 1}
a7[bits 0 to 7] ∈ {1}
[bits 8 to 31]# ∈ {97}%32, bits 8 to 31
b7 ∈ {1}
@@ -86,14 +106,23 @@
[eva:final-states] Values at end of function g:
s[0..9999999] ∈ {0; 16975879}
p_0 ∈ {{ &s + [0..39999996],0%4 }}
- c1# ∈ {0; 16975879}%32, bits 0 to 7
+ c1 ∈ {0; 7}
q ∈ {{ &s + [0..9999999] }}
- c2 ∈ {0; 1; 3; 7; 8}
+ c2 ∈ [0..8]
+[eva:final-states] Values at end of function h:
+ x ∈ [--..--]
+ i_0 ∈ [0..6]
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ {[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
@@ -108,8 +137,7 @@
i ∈ {9}
a[bits 0 to 7] ∈ {1; 6}
[bits 8 to 31]# ∈ {6}%32, bits 8 to 31
- b[bits 0 to 7] ∈ {0; 1}
- [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ b ∈ {0; 1}
a7[bits 0 to 7] ∈ {1}
[bits 8 to 31]# ∈ {97}%32, bits 8 to 31
b7 ∈ {1}
@@ -133,10 +161,16 @@
[from] Done for function f
[from] Computing for function g
[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ \result FROM min; max
[from] Function f:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -155,6 +189,8 @@
a2 FROM \nothing
[from] Function g:
s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
[from] Function main:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -183,6 +219,10 @@
s[0..9999999]; p_0; c1; q; c2
[inout] Inputs for function g:
s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
[inout] Out (internal) for function main:
TT{[0..8]; [9][bits 0 to 7]};
T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
diff --git a/tests/value/oracle/offsetmap.2.res.oracle b/tests/value/oracle/offsetmap.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..33d782cf04bc117c1285caaed11cb7033a6038b6
--- /dev/null
+++ b/tests/value/oracle/offsetmap.2.res.oracle
@@ -0,0 +1,237 @@
+[kernel] Parsing offsetmap.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ TT[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3..9] ∈ {0}
+ T[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3..9] ∈ {0}
+ i ∈ {0}
+ a ∈ {0}
+ b ∈ {0}
+ a7 ∈ {0}
+ b7 ∈ {0}
+ O1[0..19] ∈ {0}
+ O2[0..19] ∈ {0}
+ p ∈ {0}
+ x2 ∈ {0}
+ b2 ∈ {0}
+ a2 ∈ {0}
+ s[0..9999999] ∈ {0}
+[eva] computing for function f <- main.
+ Called from offsetmap.i:108.
+[eva] offsetmap.i:19: starting to merge loop iterations
+[eva] offsetmap.i:29: starting to merge loop iterations
+[eva:alarm] offsetmap.i:51: Warning:
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
+[eva] Recording results for f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from offsetmap.i:109.
+[eva:alarm] offsetmap.i:66: Warning:
+ accessing out of bounds index. assert 0 ≤ i_0;
+[eva:alarm] offsetmap.i:66: Warning:
+ accessing out of bounds index. assert i_0 < 10000000;
+[eva] Recording results for g
+[kernel] offsetmap.i:68:
+ more than 200(10000000) elements to enumerate. Approximating.
+[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ 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; 1; 256; 257}
+[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; 1; 256; 257}
+[eva] Recording results for h
+[eva] Done for function h
+[eva] Recording results for main
+[eva] Done for function main
+[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
+ {[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
+ [1][bits 0 to 7]# ∈ {0; 2}%32, bits 0 to 7
+ [1][bits 8 to 31]# ∈ {0; 2}%32, bits 8 to 31
+ [2][bits 0 to 7]# ∈ {0; 3}%32, bits 0 to 7
+ [2][bits 8 to 31]# ∈ {0; 3}%32, bits 8 to 31
+ [3..5] ∈ {0}
+ [6][bits 0 to 7]# ∈ {0; 7}%32, bits 0 to 7
+ [6][bits 8 to 31]# ∈ {0; 7}%32, bits 8 to 31
+ [7..9] ∈ {0}
+ i ∈ {9}
+ a[bits 0 to 7] ∈ {1; 6}
+ [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+ b[bits 0 to 7] ∈ {0; 1}
+ [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ a7[bits 0 to 7] ∈ {1}
+ [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+ b7 ∈ {1}
+ O1[0][bits 0 to 7] ∈ {0}
+ [0][bits 8 to 15] ∈ {18}
+ [0][bits 16 to 31] ∈ {0}
+ [1] ∈ {17}
+ [2..8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0}
+ O2[0][bits 0 to 7]# ∈ {10}%32, bits 0 to 7
+ [0][bits 8 to 15] ∈ {11}
+ [0][bits 16 to 31]# ∈ {10}%32, bits 16 to 31
+ [1..19] ∈ {0}
+ p ∈ {{ &O1[9] }}
+ x2 ∈ {1}
+ b2 ∈ {{ &x2 }}
+ a2 ∈ {{ (int)&x2 }}
+[eva:final-states] Values at end of function g:
+ s[0..9999999] ∈ {0; 16975879}
+ p_0 ∈ {{ &s + [0..39999996],0%4 }}
+ c1# ∈ {0; 16975879}%32, bits 0 to 7
+ q ∈ {{ &s + [0..9999999] }}
+ c2 ∈ {0; 1; 3; 7; 8}
+[eva:final-states] Values at end of function h:
+ x[bits 0 to 7]# ∈ {0; 42; 257}%32, bits 0 to 7
+ [bits 8 to 15]# ∈ {0; 42; 257}%32, bits 8 to 15
+ [bits 16 to 23]# ∈ {0; 42; 257}%32, bits 16 to 23
+ [bits 24 to 31]# ∈ {0; 42; 257}%32, bits 24 to 31
+ i_0 ∈ {0; 1; 2; 3; 4; 5; 6}
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ [bits 8 to 23]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 24 to 39]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 40 to 55]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 56 to 71]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 72 to 87]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 88 to 103]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 104 to 119]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
+ sp ∈ {{ &t + {1; 3; 5; 7; 9; 11; 13} }}
+[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
+ {[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
+ [1][bits 0 to 7]# ∈ {0; 2}%32, bits 0 to 7
+ [1][bits 8 to 31]# ∈ {0; 2}%32, bits 8 to 31
+ [2][bits 0 to 7]# ∈ {0; 3}%32, bits 0 to 7
+ [2][bits 8 to 31]# ∈ {0; 3}%32, bits 8 to 31
+ [3..5] ∈ {0}
+ [6][bits 0 to 7]# ∈ {0; 7}%32, bits 0 to 7
+ [6][bits 8 to 31]# ∈ {0; 7}%32, bits 8 to 31
+ [7..9] ∈ {0}
+ i ∈ {9}
+ a[bits 0 to 7] ∈ {1; 6}
+ [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+ b[bits 0 to 7] ∈ {0; 1}
+ [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ a7[bits 0 to 7] ∈ {1}
+ [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+ b7 ∈ {1}
+ O1[0][bits 0 to 7] ∈ {0}
+ [0][bits 8 to 15] ∈ {18}
+ [0][bits 16 to 31] ∈ {0}
+ [1] ∈ {17}
+ [2..8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0}
+ O2[0][bits 0 to 7]# ∈ {10}%32, bits 0 to 7
+ [0][bits 8 to 15] ∈ {11}
+ [0][bits 16 to 31]# ∈ {10}%32, bits 16 to 31
+ [1..19] ∈ {0}
+ p ∈ {{ &O1[9] }}
+ x2 ∈ {1}
+ b2 ∈ {{ &x2 }}
+ a2 ∈ {{ (int)&x2 }}
+ s[0..9999999] ∈ {0; 16975879}
+[from] Computing for function f
+[from] Done for function f
+[from] Computing for function g
+[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ \result FROM min; max
+[from] Function f:
+ TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
+ T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
+ FROM \nothing (and SELF)
+ [6] FROM b
+ i FROM \nothing
+ a FROM b
+ b FROM b (and SELF)
+ a7 FROM \nothing
+ b7 FROM \nothing
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]} FROM \nothing
+ O2[0] FROM \nothing
+ p FROM \nothing
+ x2 FROM \nothing
+ b2 FROM \nothing
+ a2 FROM \nothing
+[from] Function g:
+ s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
+[from] Function main:
+ TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
+ T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
+ FROM \nothing (and SELF)
+ [6] FROM b
+ i FROM \nothing
+ a FROM b
+ b FROM b (and SELF)
+ a7 FROM \nothing
+ b7 FROM \nothing
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]} FROM \nothing
+ O2[0] FROM \nothing
+ p FROM \nothing
+ x2 FROM \nothing
+ b2 FROM \nothing
+ a2 FROM \nothing
+ s[0..9999999] FROM i_0 (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function f:
+ TT{[0..8]; [9][bits 0 to 7]};
+ T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]}; O2[0]; p; x2; b2; a2
+[inout] Inputs for function f:
+ i; a; b; a7; p; x2; b2; a2
+[inout] Out (internal) for function g:
+ s[0..9999999]; p_0; c1; q; c2
+[inout] Inputs for function g:
+ s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
+[inout] Out (internal) for function main:
+ TT{[0..8]; [9][bits 0 to 7]};
+ T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]}; O2[0]; p; x2; b2; a2; s[0..9999999]
+[inout] Inputs for function main:
+ i; a; b; a7; p; x2; b2; a2; s{[0..9999998]; [9999999][bits 0 to 7]}
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.0.res.oracle b/tests/value/oracle_apron/offsetmap.0.res.oracle
index b718988fd802984280c4771c59c8b41e0e5ecdad..de3bcc8259f51fdbaa5cc414730f5b47e136fb58 100644
--- a/tests/value/oracle_apron/offsetmap.0.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.0.res.oracle
@@ -1,19 +1,19 @@
-64,65c64
+80,81c80
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-67,68c66
+83,84c82
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-108,109c106
+142,143c140
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-111,112c108
+145,146c142
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
diff --git a/tests/value/oracle_apron/offsetmap.1.res.oracle b/tests/value/oracle_apron/offsetmap.1.res.oracle
index 0ee129ee029e2c43453bd395a1a897d6f865e4ba..54a3c9f489329f9a6bf1d759101941258998c93a 100644
--- a/tests/value/oracle_apron/offsetmap.1.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.1.res.oracle
@@ -1,22 +1,20 @@
-64,69c64,66
+85,86c85
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+88,89c87
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
-> a ∈ {1; 6}
-> b ∈ {0; 1}
> a7 ∈ {1}
-109,114c106,108
+138,139c136
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+141,142c138
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
-> a ∈ {1; 6}
-> b ∈ {0; 1}
> a7 ∈ {1}
diff --git a/tests/value/oracle_apron/offsetmap.2.res.oracle b/tests/value/oracle_apron/offsetmap.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..52b123a5270b1f90da06bb944213992a0677b987
--- /dev/null
+++ b/tests/value/oracle_apron/offsetmap.2.res.oracle
@@ -0,0 +1,22 @@
+80,85c80,82
+< a[bits 0 to 7] ∈ {1; 6}
+< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+< b[bits 0 to 7] ∈ {0; 1}
+< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+< a7[bits 0 to 7] ∈ {1}
+< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+> b ∈ {0; 1}
+> a7 ∈ {1}
+143,148c140,142
+< a[bits 0 to 7] ∈ {1; 6}
+< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+< b[bits 0 to 7] ∈ {0; 1}
+< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+< a7[bits 0 to 7] ∈ {1}
+< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+> b ∈ {0; 1}
+> a7 ∈ {1}
diff --git a/tests/value/oracle_equality/offsetmap.2.res.oracle b/tests/value/oracle_equality/offsetmap.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44
--- /dev/null
+++ b/tests/value/oracle_equality/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
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_octagon/offsetmap.2.res.oracle b/tests/value/oracle_octagon/offsetmap.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44
--- /dev/null
+++ b/tests/value/oracle_octagon/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/offsetmap.2.res.oracle b/tests/value/oracle_symblocs/offsetmap.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
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];