diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 357ebfd681a2f55cc8dd3ab93b61e9545dac4988..495429175fba6d65763439b519f770e8cbd82a15 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -41,6 +41,10 @@ let kind_label = function
| Merge -> "Merge"
| Arith -> "Arithmetic"
+(* Ideally, we would use the current statement sid instead of the current
+ source file location. However, that would require passing the current
+ statement through any datastructures and operations that can create
+ garbled mixes, which would be an invasive change. *)
type location = Cil_datatype.Location.t
type tt =
@@ -139,9 +143,10 @@ module History_Info = struct
let size = 32
end
-(* Number of writes, number of reads, related bases. *)
-module History_Data =
- Datatype.Triple (Datatype.Int) (Datatype.Int) (Base.SetLattice)
+module LocSet = Cil_datatype.Location.Set
+
+(* Locations of writes, locations of reads, related bases. *)
+module History_Data = Datatype.Triple (LocSet) (LocSet) (Base.SetLattice)
module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
let clear () = Id.reset (); History.clear ()
@@ -154,21 +159,35 @@ let is_current = function
current location. *)
let register_write bases t =
if is_unknown t then false else
- let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
- let count, _, _ = History.memo ~change (fun _ -> 1, 0, bases) t in
- count < 2 && is_current t
+ let current_loc = Cil.CurrentLoc.get () in
+ let is_new = not (History.mem t) in
+ let change (w, r, b) =
+ LocSet.add current_loc w, r, Base.SetLattice.join b bases
+ in
+ let create _ = LocSet.singleton current_loc, LocSet.empty, bases in
+ ignore (History.memo ~change create t);
+ is_new && is_current t
(* Registers a read only if the current location is not that of the origin. *)
let register_read bases t =
if not (is_unknown t || is_current t) then
- let change (w, r, b) = w, r+1, Base.SetLattice.join b bases in
- ignore (History.memo ~change (fun _ -> 0, 1, bases) t)
+ let current_loc = Cil.CurrentLoc.get () in
+ let change (w, r, b) =
+ w, LocSet.add current_loc r, Base.SetLattice.join b bases
+ in
+ let create _ = LocSet.empty, LocSet.singleton current_loc, bases in
+ ignore (History.memo ~change create t)
(* Returns the list of recorded origins, sorted by number of reads.
Origins with no reads are filtered. *)
let get_history () =
let list = List.of_seq (History.to_seq ()) in
- let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in
+ let count (origin, (w, r, bases)) =
+ if LocSet.is_empty r
+ then None
+ else Some (origin, (LocSet.cardinal w, LocSet.cardinal r, bases))
+ in
+ let list = List.filter_map count list in
let cmp (origin1, (_, r1, _)) (origin2, (_, r2, _)) =
let r = r2 - r1 in
if r <> 0 then r else compare origin1 origin2
@@ -185,12 +204,13 @@ let pretty_origin fmt origin =
let pretty_history fmt =
let list = get_history () in
+ let plural count = if count = 1 then "" else "s" in
let pp_origin fmt (origin, (w, r, bases)) =
let bases = Base.SetLattice.filter (fun b -> not (Base.is_null b)) bases in
Format.fprintf fmt
- "@[<hov 2>%a@ (read %i times, propagated %i times)@ \
+ "@[<hov 2>%a@ (read in %i statement%s, propagated through %i statement%s)@ \
garbled mix of &%a@]"
- pretty_origin origin r w Base.SetLattice.pretty bases
+ pretty_origin origin r (plural r) w (plural w) Base.SetLattice.pretty bases
in
if list <> [] then
Format.fprintf fmt
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index ae50bf359dc8ec7fdd730f6d2635af6d25ce7453..cf45c0419b9b6fccad75b7f3d378f92617627862 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
@@ -16,7 +16,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
exceptional.i:5: arithmetic operation on addresses
- (read 3 times, propagated 3 times) garbled mix of &{i}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{i}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
diff --git a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
index 0597fca78db0c2d14ac7825ecfcc7ffbaa0c75f8..6efec9870ea80f65d22584419bd259c372760eae 100644
--- a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
@@ -25,7 +25,7 @@
(tmp from vararg)
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- Initial state (read 12 times, propagated 6 times)
+ Initial state (read in 3 statements, propagated through 3 statements)
garbled mix of &{S_0_S___va_params; S_1_S___va_params}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function sum:
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 2db3d36303765a91e701f6147e9efaacfb3e789d..bf20a0b88dbf2b4ea2db4fe6c0430c05e4c3cef9 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -29,7 +29,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
printf_garbled_mix.c:6: arithmetic operation on addresses
- (read 2 times, propagated 3 times) garbled mix of &{a}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{a}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
a[0] ∈ {1}
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index 684b949a466e6344892b87d74be20242abcbd010..54ebc9370407aa50dfdd282b12401f88086ce3a4 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -67,7 +67,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
alloc.c:26: arithmetic operation on addresses
- (read 3 times, propagated 1 times) garbled mix of &{__malloc_main_l25}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{__malloc_main_l25}
[eva] alloc.c:18: assertion 'Eva,mem_access' got final status invalid.
[eva] alloc.c:19: assertion 'Eva,mem_access' got final status invalid.
[eva] alloc.c:20: assertion 'Eva,mem_access' got final status invalid.
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index 3ce9953a7b83089a4d07f17bbecd883f451dca85..9d78cea78ca65f7bb53f13c7d32484b97ff680e7 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -33,7 +33,7 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
alloc.c:51: arithmetic operation on addresses
- (read 2 times, propagated 1 times)
+ (read in 1 statement, propagated through 1 statement)
garbled mix of &{__malloc_main_abs_l50}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main_abs:
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 4cd01a4b78eb93961e52f4939f1736ed257095bb..12f3b1ea66b34ad3c965c436a9268a36cba10676 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -67,7 +67,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
imprecise-malloc-free.c:13: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{size2}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{size2}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index d5857d6a3780f56d151fe939579bfa1bfc81ef4d..9c3b0de6adf1e40daacaf0ac128c6b426c165ecf 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -267,7 +267,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
imprecise.c:19: arithmetic operation on addresses
- (read 3 times, propagated 1 times) garbled mix of &{j; k}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{j; k}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
@@ -815,7 +816,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
imprecise.c:19: arithmetic operation on addresses
- (read 3 times, propagated 1 times) garbled mix of &{j; k}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{j; k}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index e1298461c038a1977a5d897d8e9a7a897efa1975..249e874dac1c5ca3971640c3baf12d3db698de8b 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -675,7 +675,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
strchr.c:541: arithmetic operation on addresses
- (read 1 times, propagated 3 times) garbled mix of &{x}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 043c52aa669533e1deb16aecb97093e67d3ede6e..f1e3762e46998e127a7fa8f744e42cd1eac9675b 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -287,7 +287,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index b69461ed024bb293807c22fcf863c634a5df7ae1..244530720993a3a7e052fc2c7c6f87e33eac1545 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -314,7 +314,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 05b14b3983b595fd05c1a39dcc9fb51cac2aebcb..c34017d84d4a9ae84d71a2e2f54072c4703619fd 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -288,7 +288,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index 24ccbef205c1cd4e1a182e9eb30eebea036393c0..d23a6174a0cadc609bb5457dd506babb182eb65d 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -287,7 +287,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index a0f41891c242df0ead1a4ee73efaea7f01404844..20a680fb4f8c999495bd8c39d38b551737bbc1a4 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -314,7 +314,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 25cd26ba1ee0c29e381e99198b125dd655c37124..5a90665f5e4c99e945c480c7c69d501d54c561e8 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -288,7 +288,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
nonlin.c:98: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{x_0}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 08866e9f1aa7e5bba94b7b62fabfa540d82d32a4..45ebf20af8220b7e3871dddd1592c92f74c840d9 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -255,7 +255,7 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
spawn_h.c:36: assigns clause on addresses
- (read 20 times, propagated 13 times)
+ (read in 3 statements, propagated through 2 statements)
garbled mix of &{S_argv; S_0_S_argv; S_1_S_argv}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index 2261d0849e3e6080bb275a5c6d6ea2a23ef5ef62..7ec5a5c6c38480782aa2243b7810ec1df378e6de 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -45,7 +45,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
arith_pointer.c:54: arithmetic operation on addresses
- (read 2 times, propagated 2 times) garbled mix of &{x}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{x}
[eva] arith_pointer.c:30:
assertion 'Eva,differing_blocks' got final status invalid.
[eva] ====== VALUES COMPUTED ======
@@ -158,13 +159,17 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
arith_pointer.c:54: arithmetic operation on addresses
- (read 2 times, propagated 2 times) garbled mix of &{x}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{x}
arith_pointer.c:30: arithmetic operation on addresses
- (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{x; y}
arith_pointer.c:49: arithmetic operation on addresses
- (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{x; y}
arith_pointer.c:51: arithmetic operation on addresses
- (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
t[0..1] ∈ {-3}
diff --git a/tests/value/oracle/backward_add_ptr.res.oracle b/tests/value/oracle/backward_add_ptr.res.oracle
index 35d0fce388bc2f9a9d8e16c79392d358cc71385b..5765f51b99eb38cec763b3dabfe0d0427511271c 100644
--- a/tests/value/oracle/backward_add_ptr.res.oracle
+++ b/tests/value/oracle/backward_add_ptr.res.oracle
@@ -151,7 +151,8 @@
[eva:garbled-mix:summary] Warning:
Origins of garbled mix generated during analysis:
backward_add_ptr.c:68: arithmetic operation on addresses
- (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
+ (read in 30 statements, propagated through 11 statements)
+ garbled mix of &{a; b; a; b; c}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function gm:
__retres ∈
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 6266ee5cf357f02688368950dbcf890d81a35c02..4a3b708b7a274c94b8096f7e7b49d188c44eeca7 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -449,9 +449,11 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
behaviors1.i:473: assigns clause on addresses
- (read 1 times, propagated 3 times) garbled mix of &{a}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{a}
behaviors1.i:474: assigns clause on addresses
- (read 1 times, propagated 3 times) garbled mix of &{b}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{b}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test_123_comp_2345_comp_disj:
a ∈ [--..--]
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index cae0f2d2936a0ef67c6846b8e569f6073fa67bb2..13d02bf5face0862115370d911deb7b4db158327 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -210,7 +210,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
bitfield.i:70: misaligned read of addresses
- (read 5 times, propagated 7 times) garbled mix of &{b; ee}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{b; ee}
[eva] bitfield.i:102: assertion 'Eva,initialization' got final status invalid.
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/bitwise_pointer.0.res.oracle b/tests/value/oracle/bitwise_pointer.0.res.oracle
index 6b52884383aab14b10f97928c0c5f0ad1b923ba5..dbae1b4234accb4758e5190334400a33a901082b 100644
--- a/tests/value/oracle/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.0.res.oracle
@@ -46,9 +46,11 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
bitwise_pointer.i:18: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{t}
+ (read in 1 statement, propagated through 1 statement) garbled mix of &
+ {t}
bitwise_pointer.i:22: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{t1}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{t1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0; 5}
diff --git a/tests/value/oracle/bitwise_pointer.1.res.oracle b/tests/value/oracle/bitwise_pointer.1.res.oracle
index 6b52884383aab14b10f97928c0c5f0ad1b923ba5..dbae1b4234accb4758e5190334400a33a901082b 100644
--- a/tests/value/oracle/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.1.res.oracle
@@ -46,9 +46,11 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
bitwise_pointer.i:18: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{t}
+ (read in 1 statement, propagated through 1 statement) garbled mix of &
+ {t}
bitwise_pointer.i:22: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{t1}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{t1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0; 5}
diff --git a/tests/value/oracle/context_free.res.oracle b/tests/value/oracle/context_free.res.oracle
index ba68025f931ff6945455604a0f240ca29897ba3a..e96cce61b327150eae4318bcbefb5745363e0883 100644
--- a/tests/value/oracle/context_free.res.oracle
+++ b/tests/value/oracle/context_free.res.oracle
@@ -92,7 +92,7 @@
[eva] Done for function f
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- Initial state (read 9 times, propagated 5 times)
+ Initial state (read in 7 statements, propagated through 5 statements)
garbled mix of &{WELL_uu; S_p_svoid; S_qvoid; S_0_S_vvv; S_vv}
[eva] context_free.i:62:
assertion 'Eva,function_pointer' got final status invalid.
diff --git a/tests/value/oracle/degeneration2.res.oracle b/tests/value/oracle/degeneration2.res.oracle
index e792578b81a6454041457f7b7d52776de01325ce..eff8a7e0599a4ab260d119c5ea8ba5392688487c 100644
--- a/tests/value/oracle/degeneration2.res.oracle
+++ b/tests/value/oracle/degeneration2.res.oracle
@@ -26,7 +26,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
degeneration2.i:14: arithmetic operation on addresses
- (read 6 times, propagated 1 times) garbled mix of &{B; C; D; E}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{B; C; D; E}
[eva] degeneration2.i:25:
assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/empty_struct.6.res.oracle b/tests/value/oracle/empty_struct.6.res.oracle
index cf2ce4f7e5017fc89087bc192e005d7dec7f2189..e21bc00db4f202fb511055995dbfdbd9fb54324d 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -24,7 +24,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
empty_struct.c:99: assigns clause on addresses
- (read 2 times, propagated 3 times) garbled mix of &{gs}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{gs}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main4:
r ∈
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 71ec205b2f39796fa24f19f480c7b8a685727be1..d95843418224f140e4cdbaa4cac2e80ba3d80fcc 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -719,7 +719,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
gauges.c:188: arithmetic operation on addresses
- (read 14 times, propagated 12 times) garbled mix of &{x; y}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main0:
i ∈ {1; 162}
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 49172ffd8d93700972e082185b7f3d691c1be222..7dabe5398d5293a332b7025fb2e6e1cc19738130 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -48,9 +48,11 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
imprecise_invalid_write.i:9: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{main1}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{main1}
imprecise_invalid_write.i:16: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{"abc"}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{"abc"}
[eva] imprecise_invalid_write.i:5:
assertion 'Eva,mem_access' got final status invalid.
[eva] imprecise_invalid_write.i:10:
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 150e3f1824268b9374592e59ea74da1ccc0c4429..6834f774e5734624b7a988ea43353c3c49baf858 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -234,7 +234,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
initialized.c:50: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{b4}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{b4}
[eva] initialized.c:93: assertion 'Eva,initialization' got final status invalid.
[eva] initialized.c:104:
assertion 'Eva,initialization' got final status invalid.
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index 865b2bc8486622735e111a273c8a8300c3b277a9..3541ebf53544e46e6e73c83478c87b6b09fde88a 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -143,9 +143,11 @@
[eva] Done for function main
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- leaf.i:55: assigns clause on addresses (read 10 times, propagated 2 times)
+ leaf.i:55: assigns clause on addresses
+ (read in 4 statements, propagated through 1 statement)
garbled mix of &{pg}
- leaf.i:50: assigns clause on addresses (read 4 times, propagated 2 times)
+ leaf.i:50: assigns clause on addresses
+ (read in 2 statements, propagated through 1 statement)
garbled mix of &{g}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index c03b05b96d49fc64e90e969fc0d3b0d84c0cd8fd..e648be006534144eeb94b6f672788b77498caeb6 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -24,7 +24,8 @@
[eva] Done for function main
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- leaf2.i:6: assigns clause on addresses (read 4 times, propagated 4 times)
+ leaf2.i:6: assigns clause on addresses
+ (read in 2 statements, propagated through 2 statements)
garbled mix of &{I}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 992d56c788e072721596736c0b2e43b90e331267..c5f6d20ff9c2d3815ffca02f192480d99153e54e 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -138,11 +138,14 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
library.i:31: assigns clause on addresses
- (read 2 times, propagated 2 times) garbled mix of &{S_gpi}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{S_gpi}
library.i:41: assigns clause on addresses
- (read 2 times, propagated 2 times) garbled mix of &{S_gpf}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{S_gpf}
library.i:45: assigns clause on addresses
- (read 2 times, propagated 2 times) garbled mix of &{S_gpd}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{S_gpd}
[eva] library.i:38: assertion 'Eva,function_pointer' got final status invalid.
[eva] library.i:39: assertion 'Eva,function_pointer' got final status invalid.
[eva] library.i:40: assertion 'Eva,function_pointer' got final status invalid.
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 77e8322bc7e61c9497bbd89beac20ade5492cac4..b5b12200a01466149a7326b939807eabbf565fae 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -565,7 +565,8 @@
[eva] Done for function main
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- logic.c:411: assigns clause on addresses (read 1 times, propagated 2 times)
+ logic.c:411: assigns clause on addresses
+ (read in 1 statement, propagated through 1 statement)
garbled mix of &{x_0}
[eva] logic.c:530:
Cannot evaluate range bound __fc_len - 1
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index aa7000e536dc44b7605a8c08d43d786b47352cd0..cd237bf6d63ad8d97d880ab1c2dcf0e24f33da60 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -50,10 +50,12 @@
[eva] Done for function main
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- multidim-relations.c:18: imprecise merge of addresses
- (read 7 times, propagated 0 times) garbled mix of &{g; h}
multidim-relations.c:19: imprecise merge of addresses
- (read 4 times, propagated 0 times) garbled mix of &{g; h}
+ (read in 2 statements, propagated through 0 statements)
+ garbled mix of &{g; h}
+ multidim-relations.c:18: imprecise merge of addresses
+ (read in 1 statement, propagated through 0 statements)
+ garbled mix of &{g; h}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array:
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index e93befd14488bc1553a17bdd7359fd79315a146c..bc60be868660210ec493270d4716865054f9f9df 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -200,17 +200,23 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
origin.i:19: arithmetic operation on addresses
- (read 3 times, propagated 2 times) garbled mix of &{ta2; tta2}
+ (read in 2 statements, propagated through 2 statements)
+ garbled mix of &{ta2; tta2}
origin.i:54: misaligned read of addresses
- (read 3 times, propagated 1 times) garbled mix of &{a; b}
+ (read in 2 statements, propagated through 1 statement)
+ garbled mix of &{a; b}
origin.i:14: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{ta1}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{ta1}
origin.i:25: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{ta3}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{ta3}
origin.i:100: assigns clause on addresses
- (read 2 times, propagated 2 times) garbled mix of &{S_gpp}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{S_gpp}
origin.i:48: misaligned read of addresses
- (read 2 times, propagated 1 times) garbled mix of &{a; b}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{a; b}
[eva] origin.i:75: assertion 'Eva,initialization' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index f9c473570c4ed0ed91b4da38d351db512e6bfbf2..bef2267d64184d02139971b67c3dcc6651d2c0af 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -77,7 +77,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
origin.i:126: misaligned read of addresses
- (read 1 times, propagated 2 times) garbled mix of &{x; y}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function origin:
r.c ∈ [--..--]
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index 3f7cc6e99f50ff733afed56c83c82de26a529a36..8af4494c8c1d3f713fd45c9f8d299c4a2593d442 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -97,9 +97,11 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
period.c:51: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{g}
+ (read in 1 statement, propagated through 1 statement) garbled mix of &
+ {g}
period.c:53: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{g}
+ (read in 1 statement, propagated through 1 statement) garbled mix of &
+ {g}
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index cb1dcc89815e6b7e167b7eb1a22971dcd955bda1..4d4e89341922ddd4819b2f31160b9ad12ce81287 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -242,7 +242,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
recursion.c:311: assigns clause on addresses
- (read 2 times, propagated 1 times) garbled mix of &{x; a; \copy<x>[1]}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{x; a; \copy<x>[1]}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarm:
res ∈ [10..2147483647]
diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle
index 826021d49273bf80cfb3f3e201cd0fa2cc3507dc..1779ee8c716488fdc0f783559066655c68cc23c9 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -182,7 +182,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
reduce_by_valid.i:272: assigns clause on addresses
- (read 3 times, propagated 2 times) garbled mix of &{x; a}
+ (read in 2 statements, propagated through 1 statement)
+ garbled mix of &{x; a}
[scope:rm_asserts] removing 12 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index 38218467e1391e87dd16adb079beca1594aa854e..cc754900f30ff9ebba2cfc2c8437efd4426d83df 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -64,7 +64,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
shift.i:52: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{t}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{t}
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:36: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:40: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index cf118f59bd758f7162dbcf25ddf0b285625eaa62..dc736953be952500c3174511fa4a395fbc6976f0 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -54,7 +54,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
shift.i:52: arithmetic operation on addresses
- (read 1 times, propagated 2 times) garbled mix of &{t}
+ (read in 1 statement, propagated through 2 statements)
+ garbled mix of &{t}
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:36: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:40: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index aa6a36837e24f63aa3c3f9e895594f1743c78872..0a581e91501e2a1f8d61655272280b98ff4fc6f7 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -49,7 +49,8 @@
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
sizeof.i:32: arithmetic operation on addresses
- (read 2 times, propagated 1 times) garbled mix of &{s1}
+ (read in 1 statement, propagated through 1 statement)
+ garbled mix of &{s1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
diff --git a/tests/value/oracle/va_list2.0.res.oracle b/tests/value/oracle/va_list2.0.res.oracle
index 2b3a7d3e4a6bb9f37aa3a50764303572b75e81ae..c957328829e25d2ac3d408b799ef17760dce973c 100644
--- a/tests/value/oracle/va_list2.0.res.oracle
+++ b/tests/value/oracle/va_list2.0.res.oracle
@@ -38,7 +38,7 @@
[eva] Done for function main
[eva:garbled-mix:summary]
Origins of garbled mix generated during analysis:
- Initial state (read 24 times, propagated 10 times)
+ Initial state (read in 6 statements, propagated through 4 statements)
garbled mix of &{S_0_S___va_params; S_1_S___va_params}
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/backward_add_ptr.res.oracle b/tests/value/oracle_apron/backward_add_ptr.res.oracle
index 04bf26aed2a3d76fb3e5f7a704d63846dbaab183..bc9d0f3f184d66a2ea9dbd7b881c4e8e5ecb5ee2 100644
--- a/tests/value/oracle_apron/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_apron/backward_add_ptr.res.oracle
@@ -26,7 +26,3 @@
> Called from backward_add_ptr.c:160.
> [eva] Recording results for gm
> [eva] Done for function gm
-154c166
-< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
----
-> (read 81 times, propagated 28 times) garbled mix of &{a; b; a; b; c}
diff --git a/tests/value/oracle_apron/gauges.res.oracle b/tests/value/oracle_apron/gauges.res.oracle
index fd4e06736e9b52c1034bcc0c5c67a5abef42fe89..269040aa1abf3c62135d5285883779f7cc3cb198 100644
--- a/tests/value/oracle_apron/gauges.res.oracle
+++ b/tests/value/oracle_apron/gauges.res.oracle
@@ -50,15 +50,15 @@
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
-784c771
+785c772
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-787c774
+788c775
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
-823c810
+824c811
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 5a0da48b045e46f9201b4058cfc0010bef15e6cc..cfbd463cdffd29c09f0e53feed5f870850e73e5c 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -5,32 +5,34 @@
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
< [eva:garbled-mix:write] addition.i:61: Warning:
< Assigning imprecise value to p14 because of misaligned read of addresses.
-141c135,139
+141c135,140
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
> Origins of garbled mix generated during analysis:
> addition.i:59: misaligned read of addresses
-> (read 1 times, propagated 2 times) garbled mix of &{p1}
+> (read in 1 statement, propagated through 2 statements)
+> garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-165c163
+165c164
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
-359,362d356
+359,362d357
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-368c362,366
+368c363,368
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
> Origins of garbled mix generated during analysis:
> addition.i:59: misaligned read of addresses
-> (read 1 times, propagated 2 times) garbled mix of &{p1}
+> (read in 1 statement, propagated through 2 statements)
+> garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-393c391
+393c393
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/arith_pointer.res.oracle b/tests/value/oracle_equality/arith_pointer.res.oracle
index e8d12d536a5435ae4567640619599a9d10b2e3ab..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_equality/arith_pointer.res.oracle
+++ b/tests/value/oracle_equality/arith_pointer.res.oracle
@@ -1,8 +0,0 @@
-48c48
-< (read 2 times, propagated 2 times) garbled mix of &{x}
----
-> (read 3 times, propagated 2 times) garbled mix of &{x}
-161c161
-< (read 2 times, propagated 2 times) garbled mix of &{x}
----
-> (read 3 times, propagated 2 times) garbled mix of &{x}
diff --git a/tests/value/oracle_equality/backward_add_ptr.res.oracle b/tests/value/oracle_equality/backward_add_ptr.res.oracle
index 1b7ff53fec0b3b7db573cd6fc15fa8834ae8b229..c3c184d82b0109006098a4a095481c737e2e8a92 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -23,7 +23,3 @@
> Called from backward_add_ptr.c:160.
> [eva] Recording results for gm
> [eva] Done for function gm
-154c163
-< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
----
-> (read 86 times, propagated 26 times) garbled mix of &{a; b; a; b; c}
diff --git a/tests/value/oracle_equality/bitfield.res.oracle b/tests/value/oracle_equality/bitfield.res.oracle
index d8fa5662f8993ea18aae6c740069a2253c9740e2..b7f02aef9d9234ff8d70cd49e40316983a4aed8c 100644
--- a/tests/value/oracle_equality/bitfield.res.oracle
+++ b/tests/value/oracle_equality/bitfield.res.oracle
@@ -2,7 +2,3 @@
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
-213c216
-< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
----
-> (read 6 times, propagated 7 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_equality/bitwise_pointer.0.res.oracle b/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
index 688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6..b7ca0efaf344bdb30005a1c54cccd54bd7fab3cf 100644
--- a/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
@@ -1,8 +1,8 @@
-66c66
+68c68
< x ∈ [0..9]
---
> x ∈ {5}
-79c79
+81c81
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_equality/bitwise_pointer.1.res.oracle b/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
index 688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6..b7ca0efaf344bdb30005a1c54cccd54bd7fab3cf 100644
--- a/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
@@ -1,8 +1,8 @@
-66c66
+68c68
< x ∈ [0..9]
---
> x ∈ {5}
-79c79
+81c81
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_equality/context_free.res.oracle b/tests/value/oracle_equality/context_free.res.oracle
index edf1bab4ce0f782dcf8cacb94936e89dd482ddbb..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_equality/context_free.res.oracle
+++ b/tests/value/oracle_equality/context_free.res.oracle
@@ -1,4 +0,0 @@
-95c95
-< Initial state (read 9 times, propagated 5 times)
----
-> Initial state (read 11 times, propagated 5 times)
diff --git a/tests/value/oracle_equality/empty_struct.6.res.oracle b/tests/value/oracle_equality/empty_struct.6.res.oracle
index a5fdd6006f01b6a3c868dca147b94ac07083a5ae..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_equality/empty_struct.6.res.oracle
+++ b/tests/value/oracle_equality/empty_struct.6.res.oracle
@@ -1,4 +0,0 @@
-27c27
-< (read 2 times, propagated 3 times) garbled mix of &{gs}
----
-> (read 3 times, propagated 3 times) garbled mix of &{gs}
diff --git a/tests/value/oracle_equality/gauges.res.oracle b/tests/value/oracle_equality/gauges.res.oracle
index e5c21b0c6810b8e5a50ea0dfc412e8a08fef0766..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_equality/gauges.res.oracle
+++ b/tests/value/oracle_equality/gauges.res.oracle
@@ -1,4 +0,0 @@
-722c722
-< (read 14 times, propagated 12 times) garbled mix of &{x; y}
----
-> (read 20 times, propagated 12 times) garbled mix of &{x; y}
diff --git a/tests/value/oracle_equality/origin.0.res.oracle b/tests/value/oracle_equality/origin.0.res.oracle
index a12449e315cdcbf000a4adcafec176f044d53066..9c85d7de249081d860e467bd51f94c8c1a757050 100644
--- a/tests/value/oracle_equality/origin.0.res.oracle
+++ b/tests/value/oracle_equality/origin.0.res.oracle
@@ -1,9 +1,9 @@
-246,247c246
+252,253c252
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
-281,282c280
+287,288c286
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
diff --git a/tests/value/oracle_equality/period.res.oracle b/tests/value/oracle_equality/period.res.oracle
index 657c13125d1d186b4e4b752cd479fb28e639a08b..54f6fc44b0d4c8cf5be9e39d50eb248bd42f4eeb 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -4,7 +4,8 @@
< [eva:garbled-mix:write] period.c:53:
< Assigning imprecise value to p because of arithmetic operation on addresses.
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
-101,103d95
+102,105d96
< period.c:53: arithmetic operation on addresses
-< (read 2 times, propagated 1 times) garbled mix of &{g}
+< (read in 1 statement, propagated through 1 statement) garbled mix of &
+< {g}
< [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_equality/va_list2.0.res.oracle b/tests/value/oracle_equality/va_list2.0.res.oracle
index 2907faaa45d2cec4207024217ed66cf9699b41f8..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_equality/va_list2.0.res.oracle
+++ b/tests/value/oracle_equality/va_list2.0.res.oracle
@@ -1,4 +0,0 @@
-41c41
-< Initial state (read 24 times, propagated 10 times)
----
-> Initial state (read 28 times, propagated 10 times)
diff --git a/tests/value/oracle_gauges/bitfield.res.oracle b/tests/value/oracle_gauges/bitfield.res.oracle
index 619b7b85a2389c7c7816e21f58c56851130dcdb0..6bff95a7cf72715f871fc23bdef8b3a865305b41 100644
--- a/tests/value/oracle_gauges/bitfield.res.oracle
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -14,7 +14,3 @@
> [eva] bitfield.i:73:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
-213c228
-< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
----
-> (read 9 times, propagated 11 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle
index ded703ccb200de2e23ff4878b4831319fce4b033..0b8798617c76f22cfd19fe7d5427e6a2613da3f0 100644
--- a/tests/value/oracle_gauges/gauges.res.oracle
+++ b/tests/value/oracle_gauges/gauges.res.oracle
@@ -263,52 +263,48 @@
714a835,836
> [eva] gauges.c:343: Call to builtin malloc
> [eva] gauges.c:343: Call to builtin malloc
-722c844
-< (read 14 times, propagated 12 times) garbled mix of &{x; y}
----
-> (read 12 times, propagated 11 times) garbled mix of &{x; y}
-771,772c893,894
+772,773c894,895
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
-784c906
+785c907
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-790c912
+791c913
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-796c918
+797c919
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-816c938
+817c939
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-818c940
+819c941
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-823c945
+824c946
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-834,835c956,958
+835,836c957,959
< [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
< p ∈ {{ &y + [4..40],0%4 }}
---
> [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
> [7..9] ∈ UNINITIALIZED
> p ∈ {{ &y[7] }}
-846c969
+847c970
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-851,855c974
+852,856c975
< n ∈ {0}
< arr[0] ∈ {0}
< [1] ∈ {-1}
@@ -316,19 +312,19 @@
< p ∈ {{ &arr + [12..--],0%4 }}
---
> NON TERMINATING FUNCTION
-958a1078
+959a1079
> [from] Non-terminating function main8_aux (no dependencies)
-981,982c1101,1102
+982,983c1102,1103
< p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF)
< \result FROM p; A; B; n; p; A[0..9]; B[0..9]
---
> p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF)
> \result FROM p; A; B; n; p; A[0..8]; B[0..8]
-1026c1146
+1027c1147
< NO EFFECTS
---
> NON TERMINATING - NO EFFECTS
-1060c1180
+1061c1181
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
diff --git a/tests/value/oracle_gauges/va_list2.0.res.oracle b/tests/value/oracle_gauges/va_list2.0.res.oracle
index 70defd3cb22fe585b3ac25d1cbc4a5509d95456b..80fc106a63e0bc09c6ccf89c3f85ddb2cca12acd 100644
--- a/tests/value/oracle_gauges/va_list2.0.res.oracle
+++ b/tests/value/oracle_gauges/va_list2.0.res.oracle
@@ -11,7 +11,3 @@
> [eva] va_list2.c:21:
> Frama_C_show_each_f:
> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
-41c53
-< Initial state (read 24 times, propagated 10 times)
----
-> Initial state (read 36 times, propagated 16 times)
diff --git a/tests/value/oracle_octagon/bitfield.res.oracle b/tests/value/oracle_octagon/bitfield.res.oracle
index d8fa5662f8993ea18aae6c740069a2253c9740e2..b7f02aef9d9234ff8d70cd49e40316983a4aed8c 100644
--- a/tests/value/oracle_octagon/bitfield.res.oracle
+++ b/tests/value/oracle_octagon/bitfield.res.oracle
@@ -2,7 +2,3 @@
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
-213c216
-< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
----
-> (read 6 times, propagated 7 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle
index acb804905135c794b100d1f8ccc6e91305a36faa..70f56d52bf5421e510c5b536b8cd02aecb1f2cbd 100644
--- a/tests/value/oracle_octagon/gauges.res.oracle
+++ b/tests/value/oracle_octagon/gauges.res.oracle
@@ -7,11 +7,11 @@
< [eva] gauges.c:218: Frama_C_show_each:
< [eva:alarm] gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-773c766
+774c767
< numNonZero ∈ [-2147483648..8]
---
> numNonZero ∈ {-1}
-784c777
+785c778
< n ∈ [-2147483648..99]
---
> n ∈ {-1}
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
index 688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6..b7ca0efaf344bdb30005a1c54cccd54bd7fab3cf 100644
--- a/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
@@ -1,8 +1,8 @@
-66c66
+68c68
< x ∈ [0..9]
---
> x ∈ {5}
-79c79
+81c81
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
index 688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6..b7ca0efaf344bdb30005a1c54cccd54bd7fab3cf 100644
--- a/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
@@ -1,8 +1,8 @@
-66c66
+68c68
< x ∈ [0..9]
---
> x ∈ {5}
-79c79
+81c81
< x1 ∈ [0..9]
---
> x1 ∈ {5}