diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index 47e5fcec857fbf529aa684071565deb0082297fb..ae50bf359dc8ec7fdd730f6d2635af6d25ce7453 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
@@ -13,6 +13,10 @@
signed overflow. assert a + x ≤ 2147483647;
[eva:alarm] exceptional.i:23: Warning:
signed overflow. assert (int)(a + x) + (int)c ≤ 2147483647;
+[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}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index 44a3cdfd58d00b48dd99a2a3a393754880497e23..201d2b2a599aa089c5debb92d71b0fd2e6d33d98 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -18,6 +18,9 @@
[eva] using specification for function __e_acsl_full_init
[eva] using specification for function __e_acsl_valid
[eva] using specification for function __e_acsl_assert_register_ptr
+[eva:garbled-mix:assigns] issue-eacsl-145.c:9:
+ The specification of function __e_acsl_assert_register_ptr
+ has generated a garbled mix of addresses for assigns clause data->values.
[eva] using specification for function __e_acsl_assert_register_ulong
[eva:alarm] issue-eacsl-145.c:9: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index 88f3fdf2c69e4beb452975bb5a5f9f465402c9b9..d1c33a8a5ee375b35ac4c016138ba4181b58cfd3 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -96,9 +96,9 @@ let wkey_locals_escaping = register_warn_category "locals-escaping"
let wkey_garbled_mix_write = register_warn_category "garbled-mix:write"
let () = set_warn_status wkey_garbled_mix_write Log.Wfeedback
let wkey_garbled_mix_assigns = register_warn_category "garbled-mix:assigns"
-let () = set_warn_status wkey_garbled_mix_assigns Log.Winactive
+let () = set_warn_status wkey_garbled_mix_assigns Log.Wfeedback
let wkey_garbled_mix_summary = register_warn_category "garbled-mix:summary"
-let () = set_warn_status wkey_garbled_mix_summary Log.Winactive
+let () = set_warn_status wkey_garbled_mix_summary Log.Wfeedback
let wkey_builtins_missing_spec = register_warn_category "builtins:missing-spec"
let wkey_builtins_override = register_warn_category "builtins:override"
let wkey_libc_unsupported_spec = register_warn_category "libc:unsupported-spec"
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 d8fbec93f6a55d50d7bd4c804afc9b29b796c593..0597fca78db0c2d14ac7825ecfcc7ffbaa0c75f8 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
@@ -23,6 +23,10 @@
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow. assert ret + tmp ≤ 2147483647;
(tmp from vararg)
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 12 times, propagated 6 times)
+ 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:
ret ∈
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 74ea04f2c8f1a5bfd993c56fc4632ae881ab3cb7..335dfe32f04bc71a0f8347d6161575ecc33dbca2 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -20,8 +20,20 @@
Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] using specification for function execve
+[eva:garbled-mix:assigns] exec.c:9:
+ The specification of function execve has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] using specification for function execv
+[eva:garbled-mix:assigns] exec.c:11:
+ The specification of function execv has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] using specification for function execvp
+[eva:garbled-mix:assigns] exec.c:12:
+ The specification of function execvp has generated a garbled mix of addresses
+ for assigns clause \result.
+[eva:garbled-mix:assigns] exec.c:13:
+ The specification of function execve has generated a garbled mix of addresses
+ for assigns clause \result.
[kernel:annot:missing-spec] exec.c:15: Warning:
Neither code nor specification for function execlp_fallback_1,
generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index efb382209ebc308a4db702b55202f52ddb07650f..7b945647be0216ee15d342ea55494da9642fb01b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -114,6 +114,10 @@
[eva] using specification for function printf_va_23
[eva] using specification for function printf_va_24
[eva] using specification for function printf_va_25
+[eva:garbled-mix:assigns] printf.c:68:
+ The specification of function printf_va_25
+ has generated a garbled mix of addresses
+ for assigns clause __fc_stdout->__fc_FILE_data.
[eva] using specification for function printf_va_26
[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf_fallback_1,
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 55f26985dfe052afb8beee70b695b23c87f304a6..2db3d36303765a91e701f6147e9efaacfb3e789d 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
@@ -26,6 +26,10 @@
[eva] using specification for function printf_va_1
[eva] printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
+[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}
[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 7ce75e72f2118a378e84e5ca5e3a13f8e7e6ec51..684b949a466e6344892b87d74be20242abcbd010 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -64,6 +64,10 @@
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 7633c770d7101f16479f5b2848e9463500ce44eb..77bfca7bbb74e166fbde9bb07f945257115aeb0c 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -30,6 +30,11 @@
[eva:alarm] alloc.c:56: Warning: signed overflow. assert *q + 1 ≤ 2147483647;
[eva] Recording results for main_abs
[eva] Done for function main_abs
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ alloc.c:51: arithmetic operation on addresses
+ (read 2 times, propagated 1 times)
+ garbled mix of &{__malloc_main_abs_l50}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main_abs:
NULL[rbits 2048 to 4103] ∈
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 7134efd0323fd61d6cebbd58fa02929b0c856620..4cd01a4b78eb93961e52f4939f1736ed257095bb 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -64,6 +64,10 @@
weak free on bases: {__malloc_main_l15, __malloc_main_l16}
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 ec7cb60e6e250de7e3d20234f69876cd67fd2b20..1ad813d673e5c5dc6276df115ec2a8b78663aed0 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -264,6 +264,10 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise.c:19: arithmetic operation on addresses
+ (read 3 times, propagated 1 times) garbled mix of &{j; k}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
@@ -807,6 +811,10 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise.c:19: arithmetic operation on addresses
+ (read 3 times, propagated 1 times) 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/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 16a5a8ec3b5bbdf8045da8874b28335e0b4bc819..c97ebeb2a70161b6c360d6cb8bf94962bf92fb3f 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -806,6 +806,10 @@
Called from linked_list.c:51.
[eva] using specification for function printf_va_1
[eva] linked_list.c:51: function printf_va_1: precondition got status valid.
+[eva:garbled-mix:assigns] linked_list.c:51:
+ The specification of function printf_va_1
+ has generated a garbled mix of addresses
+ for assigns clause __fc_stdout->__fc_FILE_data.
[eva] Done for function printf_va_1
[kernel] linked_list.c:51:
more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index ffbebfd90e0f629e11045f9b18f3ead6506ec7fd..e1298461c038a1977a5d897d8e9a7a897efa1975 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -672,6 +672,10 @@
[eva] Done for function strchr_garbled_mix_in_char
[eva] Recording results for main
[eva] Done for function main
+[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}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
diff --git a/tests/builtins/oracle_equality/linked_list.1.res.oracle b/tests/builtins/oracle_equality/linked_list.1.res.oracle
index dc1c07fbca0f6ce44824d4bdff2b3cf9110babd1..08a077ea283d0d72948ad4ac7cc139699f42818e 100644
--- a/tests/builtins/oracle_equality/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_equality/linked_list.1.res.oracle
@@ -16,9 +16,9 @@
720a731,732
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d821
+814,815d825
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d828
+823,824d832
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_gauges/linked_list.1.res.oracle b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
index ec6dff88c11d22b8f7b5764d51fe82406d5cd9e0..b4dd8f6901bfedbeff231430246bb6c77f704f48 100644
--- a/tests/builtins/oracle_gauges/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
@@ -1,4 +1,4 @@
-817a818,823
+821a822,827
> [eva] computing for function printf_va_1 <- main.
> Called from linked_list.c:51.
> [eva] Done for function printf_va_1
diff --git a/tests/builtins/oracle_octagon/linked_list.1.res.oracle b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
index 4083e687dd36eae966d07c6feea16e88f79ce698..166d64faad77cf59fe2003c8dda6ac23d5adf97d 100644
--- a/tests/builtins/oracle_octagon/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
@@ -10,9 +10,9 @@
720a727,728
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d817
+814,815d821
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d824
+823,824d828
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
index 4083e687dd36eae966d07c6feea16e88f79ce698..166d64faad77cf59fe2003c8dda6ac23d5adf97d 100644
--- a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
@@ -10,9 +10,9 @@
720a727,728
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d817
+814,815d821
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d824
+823,824d828
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 04ffb0d077bb56f347f3db8d9e4dfaf8f22ff2d4..043c52aa669533e1deb16aecb97093e67d3ede6e 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -284,6 +284,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 54cd152e82f21b5e75ea73f7a715a804f8a72f45..b69461ed024bb293807c22fcf863c634a5df7ae1 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -311,6 +311,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 9ae60320eb162865fb9e2dfe8d15991d5b1056e9..05b14b3983b595fd05c1a39dcc9fb51cac2aebcb 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -285,6 +285,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 17b03c98f92314bff3fe61bb303196e9eefb2872..24ccbef205c1cd4e1a182e9eb30eebea036393c0 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -284,6 +284,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 33877fa4e0891cf6f0918b35f8dc656feda4c369..a0f41891c242df0ead1a4ee73efaea7f01404844 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -311,6 +311,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 66c509fd9b8fef46e8dd64ddeadb67f0bf563877..25cd26ba1ee0c29e381e99198b125dd655c37124 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -285,6 +285,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[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}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
diff --git a/tests/libc/oracle/pwd_h.res.oracle b/tests/libc/oracle/pwd_h.res.oracle
index 6cdda1a2be90568192afabc4b31d25b32fbdfb21..5dedb215f1a912fec633ab2a5558fcae72075554 100644
--- a/tests/libc/oracle/pwd_h.res.oracle
+++ b/tests/libc/oracle/pwd_h.res.oracle
@@ -7,6 +7,9 @@
[eva] computing for function getpwuid <- main.
Called from pwd_h.c:10.
[eva] using specification for function getpwuid
+[eva:garbled-mix:assigns] pwd_h.c:10:
+ The specification of function getpwuid
+ has generated a garbled mix of addresses for assigns clause __fc_pwd.
[eva] Done for function getpwuid
[eva:alarm] pwd_h.c:13: Warning: assertion got status unknown.
[eva:alarm] pwd_h.c:14: Warning: assertion got status unknown.
@@ -16,6 +19,9 @@
Called from pwd_h.c:18.
[eva] using specification for function getpwnam
[eva] pwd_h.c:18: function getpwnam: precondition 'valid_name' got status valid.
+[eva:garbled-mix:assigns] pwd_h.c:18:
+ The specification of function getpwnam
+ has generated a garbled mix of addresses for assigns clause __fc_pwd.
[eva] Done for function getpwnam
[eva:alarm] pwd_h.c:21: Warning: assertion got status unknown.
[eva:alarm] pwd_h.c:22: Warning: assertion got status unknown.
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 1b2258ac3dd8070c2a6b0238ec9b15a848fab49c..fe4f9414bf77cb385fed69ef556d573f56ec2282 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -112,6 +112,9 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:45:
function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva:garbled-mix:assigns] signal_h.c:45:
+ The specification of function sigaction
+ has generated a garbled mix of addresses for assigns clause *oldact.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:45.
@@ -128,6 +131,9 @@
function sigaction: precondition 'separation,separated_acts' got status valid.
[eva] FRAMAC_SHARE/libc/signal.h:229:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
+[eva:garbled-mix:assigns] signal_h.c:48:
+ The specification of function sigaction
+ has generated a garbled mix of addresses for assigns clause *oldact.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:51.
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 4b4c978087e9754cede4451980d1dae737d7f9d0..08866e9f1aa7e5bba94b7b62fabfa540d82d32a4 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -7,6 +7,9 @@
[eva] computing for function getopt <- main.
Called from spawn_h.c:36.
[eva] using specification for function getopt
+[eva:garbled-mix:assigns] spawn_h.c:36:
+ The specification of function getopt has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function getopt
[kernel:annot:missing-spec] spawn_h.c:43: Warning:
Neither code nor specification for function posix_spawn_file_actions_init,
@@ -249,6 +252,11 @@
[eva] Done for function exit
[eva] Recording results for main
[eva] Done for function main
+[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)
+ 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:
NON TERMINATING FUNCTION
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 24a810167ef1b8fa7ffc5041926c514863c09381..46a982f0c8014eaa284a7352d3f8664f99dcadbe 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -58,6 +58,9 @@
function execv: precondition 'valid_string_path' got status valid.
[eva] unistd_h.c:17:
function execv: precondition 'valid_string_argv0' got status valid.
+[eva:garbled-mix:assigns] unistd_h.c:17:
+ The specification of function execv has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function execv
[eva] computing for function execv <- main.
Called from unistd_h.c:17.
diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle
index 8b074bf06abdd613754931d1720a4884ceb3f673..7ba1874acead31fd20c084a227d3c52fa55f6fac 100644
--- a/tests/slicing/oracle/loops.10.res.oracle
+++ b/tests/slicing/oracle/loops.10.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.19.res.oracle b/tests/slicing/oracle/loops.19.res.oracle
index 34457cfad25d07e2868e3518708480733f7473fa..0998264ade13e755871e320c9cd50baadbcf6c06 100644
--- a/tests/slicing/oracle/loops.19.res.oracle
+++ b/tests/slicing/oracle/loops.19.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.20.res.oracle b/tests/slicing/oracle/loops.20.res.oracle
index 27d8cdb835562da76ec04f76f72017aa7aaba1b0..6e18bd872d2d86d795df7d8d77af2cc984dd6a76 100644
--- a/tests/slicing/oracle/loops.20.res.oracle
+++ b/tests/slicing/oracle/loops.20.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle
index 9adf543884b06243c38d066d660dce7d01610e18..8636ad07b17046ce79ca5ca1ab0eb519c01bf81c 100644
--- a/tests/slicing/oracle/loops.21.res.oracle
+++ b/tests/slicing/oracle/loops.21.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle
index 7d41e9a40cdb66446abcee9448378d0a0ddbef06..3313fbc32d943908d3b6701ed97fdd379ff18096 100644
--- a/tests/slicing/oracle/loops.22.res.oracle
+++ b/tests/slicing/oracle/loops.22.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.23.res.oracle b/tests/slicing/oracle/loops.23.res.oracle
index 24eb43a90cba0b80c99d1795f5b1566d2443857b..ae8f97a78fc3c8b783c571ad7895d4ad8ea25d81 100644
--- a/tests/slicing/oracle/loops.23.res.oracle
+++ b/tests/slicing/oracle/loops.23.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.8.res.oracle b/tests/slicing/oracle/loops.8.res.oracle
index 3c7880c3af1ec26d5a6c78fa64382ce48b28eaf5..f1d9bbd86696821f18cab14e3276c13346963cb5 100644
--- a/tests/slicing/oracle/loops.8.res.oracle
+++ b/tests/slicing/oracle/loops.8.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle
index abc0b21b556922c6b9b00615dfba3fe01f412bbb..a2caa35921cfccd62af77a1b13f943464086f2cd 100644
--- a/tests/slicing/oracle/loops.9.res.oracle
+++ b/tests/slicing/oracle/loops.9.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index d8c8908c4b6586ae2f6baa6b01cca727b28032c3..2261d0849e3e6080bb275a5c6d6ea2a23ef5ef62 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -42,6 +42,10 @@
[eva] Done for function main2
[eva] Recording results for main
[eva] Done for function main
+[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}
[eva] arith_pointer.c:30:
assertion 'Eva,differing_blocks' got final status invalid.
[eva] ====== VALUES COMPUTED ======
@@ -151,6 +155,16 @@
[eva] Done for function main2
[eva] Recording results for main
[eva] Done for function main
+[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}
+ arith_pointer.c:30: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ arith_pointer.c:49: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ arith_pointer.c:51: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) 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/assign-leaf-indirect.res.oracle b/tests/value/oracle/assign-leaf-indirect.res.oracle
index d1632315bcb6bce72993ab83ee145e4ba4229247..4d4a939a92b3718e5132e1408fe9eef94151bfa8 100644
--- a/tests/value/oracle/assign-leaf-indirect.res.oracle
+++ b/tests/value/oracle/assign-leaf-indirect.res.oracle
@@ -9,6 +9,9 @@
[eva] computing for function f <- main.
Called from assign-leaf-indirect.i:8.
[eva] using specification for function f
+[eva:garbled-mix:assigns] assign-leaf-indirect.i:8:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause y.
[eva] Done for function f
[eva] computing for function g <- main.
Called from assign-leaf-indirect.i:9.
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index 002087f31ba8abd39638d82d19e0589a787a698a..55b41ae8a07167bd77b0ccba4956bae60544cb17 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -298,6 +298,9 @@
[eva] computing for function f18 <- main18 <- main.
Called from assigns_from.i:215.
[eva] using specification for function f18
+[eva:garbled-mix:assigns] assigns_from.i:215:
+ The specification of function f18 has generated a garbled mix of addresses
+ for assigns clause *x.
[eva] Done for function f18
[eva] Recording results for main18
[from] Computing for function main18
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index c434339fdecb7a85c1faef91c8aaa1b4215613e3..6266ee5cf357f02688368950dbcf890d81a35c02 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -305,9 +305,15 @@
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:473.
[eva] using specification for function f
+[eva:garbled-mix:assigns] behaviors1.i:473:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:474.
+[eva:garbled-mix:assigns] behaviors1.i:474:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:475.
@@ -440,6 +446,12 @@
[eva] Done for function test_narrow
[eva] Recording results for main
[eva] Done for function main
+[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}
+ behaviors1.i:474: assigns clause on addresses
+ (read 1 times, propagated 3 times) 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 3b980d881cf63089d57219cca678788e03fa5090..3751001cbba46ff03930675e67332c3686863ee2 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -105,6 +105,9 @@
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
Called from bitfield.i:70.
[eva] using specification for function leaf
+[eva:garbled-mix:assigns] bitfield.i:70:
+ The specification of function leaf has generated a garbled mix of addresses
+ for assigns clause *p1.
[eva] Done for function leaf
[eva] bitfield.i:71:
Frama_C_show_each:
@@ -204,6 +207,10 @@
[eva] Done for function char_short
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 aa3a3f4a6a294519cff95e18f53878fc7c85bdc7..6b52884383aab14b10f97928c0c5f0ad1b923ba5 100644
--- a/tests/value/oracle/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.0.res.oracle
@@ -43,6 +43,12 @@
out of bounds write. assert \valid(p1);
[eva] Recording results for main
[eva] Done for function main
+[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}
+ bitwise_pointer.i:22: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) 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 aa3a3f4a6a294519cff95e18f53878fc7c85bdc7..6b52884383aab14b10f97928c0c5f0ad1b923ba5 100644
--- a/tests/value/oracle/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.1.res.oracle
@@ -43,6 +43,12 @@
out of bounds write. assert \valid(p1);
[eva] Recording results for main
[eva] Done for function main
+[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}
+ bitwise_pointer.i:22: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) 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 ffee5073affe361f3df6aa1b3baa894953b95853..ba68025f931ff6945455604a0f240ca29897ba3a 100644
--- a/tests/value/oracle/context_free.res.oracle
+++ b/tests/value/oracle/context_free.res.oracle
@@ -90,6 +90,10 @@
pointer to function with incompatible type. assert \valid_function(g);
[eva] Recording results for f
[eva] Done for function f
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 9 times, propagated 5 times)
+ 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.
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/degeneration2.res.oracle b/tests/value/oracle/degeneration2.res.oracle
index de456405cd98bad14e79ef22e9aa5c1c924883e3..e792578b81a6454041457f7b7d52776de01325ce 100644
--- a/tests/value/oracle/degeneration2.res.oracle
+++ b/tests/value/oracle/degeneration2.res.oracle
@@ -23,6 +23,10 @@
accessing uninitialized left-value. assert \initialized(&offset_uninit);
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 88263f19b58274baed0cb0b4ce28206a3abe4b8a..cf2ce4f7e5017fc89087bc192e005d7dec7f2189 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -8,6 +8,9 @@
[eva] computing for function f <- main4.
Called from empty_struct.c:99.
[eva] using specification for function f
+[eva:garbled-mix:assigns] empty_struct.c:99:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
[kernel:annot:missing-spec] empty_struct.c:100: Warning:
Neither code nor specification for function g,
@@ -18,6 +21,10 @@
[eva] Done for function g
[eva] Recording results for main4
[eva] Done for function main4
+[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}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main4:
r ∈
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index 88c6c5d8c6d416983f927de6f9655687531bbebf..f3377d39ae638c90c299fa32083c399803a221ef 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -178,6 +178,9 @@
[eva] computing for function unavailable_f <- main.
Called from from_call.i:96.
[eva] using specification for function unavailable_f
+[eva:garbled-mix:assigns] from_call.i:96:
+ The specification of function unavailable_f
+ has generated a garbled mix of addresses for assigns clause AR.
[eva] Done for function unavailable_f
[eva] Recording results for main
[from] Computing for function main
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index 560d21d929a84ba7eec01b95ef43454445de32a5..18901931cee6b75386e480ca4f21c8681cb5955b 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -142,6 +142,9 @@
[eva] computing for function unavailable_f <- main.
Called from from_call.i:96.
[eva] using specification for function unavailable_f
+[eva:garbled-mix:assigns] from_call.i:96:
+ The specification of function unavailable_f
+ has generated a garbled mix of addresses for assigns clause AR.
[eva] Done for function unavailable_f
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index ce2c46bcca8652340104e25017c95045abc3dad6..4b7f0372dd0bb9eb70ae5e95a7ad3d083f33c162 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -710,6 +710,10 @@
[eva] Done for function main17
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 3b45112de2a37cad0bd4d80efe85f58d07634ff4..49172ffd8d93700972e082185b7f3d691c1be222 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -45,6 +45,12 @@
[eva] Done for function main3
[eva] Recording results for main
[eva] Done for function main
+[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}
+ imprecise_invalid_write.i:16: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) 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 1e822fd04fadadcd9e7fc2f60b1057b75e3cb553..150e3f1824268b9374592e59ea74da1ccc0c4429 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -231,6 +231,10 @@
[eva] Done for function reduce_by_negation
[eva] Recording results for main
[eva] Done for function main
+[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}
[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/inout_proto.res.oracle b/tests/value/oracle/inout_proto.res.oracle
index 77fcb77f70191983ad3627233361879ec9e288a7..d96ee3689cbfcaf14df1fbc700e908385e2a6247 100644
--- a/tests/value/oracle/inout_proto.res.oracle
+++ b/tests/value/oracle/inout_proto.res.oracle
@@ -13,6 +13,9 @@
[eva] computing for function SendBuffer <- main <- main_main.
Called from inout_proto.i:19.
[eva] using specification for function SendBuffer
+[eva:garbled-mix:assigns] inout_proto.i:19:
+ The specification of function SendBuffer
+ has generated a garbled mix of addresses for assigns clause *RETURN_CODE.
[eva] Done for function SendBuffer
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index d966184b444f1e6e55c2678426d0e103d88c926c..865b2bc8486622735e111a273c8a8300c3b277a9 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -39,6 +39,9 @@
[eva] computing for function f_int_star_int <- main.
Called from leaf.i:50.
[eva] using specification for function f_int_star_int
+[eva:garbled-mix:assigns] leaf.i:50:
+ The specification of function f_int_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_int_star_int
[eva] leaf.i:51: Frama_C_show_each_F: [-2147483648..2147483647]
[eva:alarm] leaf.i:52: Warning: out of bounds write. assert \valid(p);
@@ -46,6 +49,9 @@
[eva] computing for function f_int_star_int_star_int <- main.
Called from leaf.i:55.
[eva] using specification for function f_int_star_int_star_int
+[eva:garbled-mix:assigns] leaf.i:55:
+ The specification of function f_int_star_int_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_int_star_int_star_int
[eva] leaf.i:56: Frama_C_show_each_G: {{ &g }}
[eva] leaf.i:57: Frama_C_show_each_F: {5}
@@ -85,6 +91,9 @@
[eva] computing for function f_st_star_cint_st_star_cint <- main.
Called from leaf.i:68.
[eva] using specification for function f_st_star_cint_st_star_cint
+[eva:garbled-mix:assigns] leaf.i:68:
+ The specification of function f_st_star_cint_st_star_cint
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_st_star_cint_st_star_cint
[kernel:annot:missing-spec] leaf.i:69: Warning:
Neither code nor specification for function f_st_star_int_st_star_int,
@@ -92,6 +101,9 @@
[eva] computing for function f_st_star_int_st_star_int <- main.
Called from leaf.i:69.
[eva] using specification for function f_st_star_int_st_star_int
+[eva:garbled-mix:assigns] leaf.i:69:
+ The specification of function f_st_star_int_st_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_st_star_int_st_star_int
[kernel:annot:missing-spec] leaf.i:70: Warning:
Neither code nor specification for function f_st_tab3_int_st_tab3_int,
@@ -106,6 +118,9 @@
[eva] computing for function f_star_st_star_cint_int <- main.
Called from leaf.i:72.
[eva] using specification for function f_star_st_star_cint_int
+[eva:garbled-mix:assigns] leaf.i:72:
+ The specification of function f_star_st_star_cint_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_st_star_cint_int
[kernel:annot:missing-spec] leaf.i:73: Warning:
Neither code nor specification for function f_star_st_star_int_int,
@@ -113,6 +128,9 @@
[eva] computing for function f_star_st_star_int_int <- main.
Called from leaf.i:73.
[eva] using specification for function f_star_st_star_int_int
+[eva:garbled-mix:assigns] leaf.i:73:
+ The specification of function f_star_st_star_int_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_st_star_int_int
[kernel:annot:missing-spec] leaf.i:74: Warning:
Neither code nor specification for function f_star_st_tab3_int_int,
@@ -123,6 +141,12 @@
[eva] Done for function f_star_st_tab3_int_int
[eva] Recording results for main
[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)
+ garbled mix of &{pg}
+ leaf.i:50: assigns clause on addresses (read 4 times, propagated 2 times)
+ garbled mix of &{g}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
T[0] ∈ [--..--]
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 5de89a4124f3730f3cb7fca1093681bd40c29c3a..c03b05b96d49fc64e90e969fc0d3b0d84c0cd8fd 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -14,11 +14,18 @@
[eva] computing for function f <- main.
Called from leaf2.i:6.
[eva] using specification for function f
+[eva:garbled-mix:assigns] leaf2.i:6:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
[eva:alarm] leaf2.i:7: Warning: signed overflow. assert -2147483648 ≤ G + 1;
[eva:alarm] leaf2.i:7: Warning: signed overflow. assert G + 1 ≤ 2147483647;
[eva] Recording results for main
[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)
+ garbled mix of &{I}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
G ∈ {{ garbled mix of &{I} (origin: Library function {leaf2.i:6}) }}
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 01756f25fda5661297a36cda69ec139a857140c8..992d56c788e072721596736c0b2e43b90e331267 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -86,6 +86,9 @@
[eva] computing for function f_star_int <- main.
Called from library.i:31.
[eva] using specification for function f_star_int
+[eva:garbled-mix:assigns] library.i:31:
+ The specification of function f_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_int
[eva:alarm] library.i:32: Warning: out of bounds write. assert \valid(G1);
[eva:alarm] library.i:33: Warning: out of bounds read. assert \valid_read(G);
@@ -109,6 +112,9 @@
[eva] computing for function i <- main.
Called from library.i:41.
[eva] using specification for function i
+[eva:garbled-mix:assigns] library.i:41:
+ The specification of function i has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function i
[eva:alarm] library.i:42: Warning: out of bounds read. assert \valid_read(pf);
[eva:alarm] library.i:42: Warning:
@@ -122,10 +128,21 @@
[eva] computing for function k <- main.
Called from library.i:45.
[eva] using specification for function k
+[eva:garbled-mix:assigns] library.i:45:
+ The specification of function k has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function k
[eva:alarm] library.i:46: Warning: out of bounds write. assert \valid(pd);
[eva] Recording results for main
[eva] Done for function main
+[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}
+ library.i:41: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpf}
+ library.i:45: assigns clause on addresses
+ (read 2 times, propagated 2 times) 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 cc514176b48a155bf2b67d375b61cbad018df839..77e8322bc7e61c9497bbd89beac20ade5492cac4 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -415,6 +415,9 @@
[eva] logic.c:408: Frama_C_show_each_set: {0; 1; 2; 3; 4; 5}
[eva] computing for function abs <- int_abs <- main.
Called from logic.c:411.
+[eva:garbled-mix:assigns] logic.c:411:
+ The specification of function abs has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function abs
[eva] logic.c:412:
Frama_C_show_each_gm:
@@ -560,6 +563,10 @@
[eva] Done for function plet
[eva] Recording results for main
[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)
+ garbled mix of &{x_0}
[eva] logic.c:530:
Cannot evaluate range bound __fc_len - 1
(unsupported logic var __fc_len). Approximating
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index e7f1d9da7ace7a3640b02aab980928a144b93e12..aa7000e536dc44b7605a8c08d43d786b47352cd0 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -48,6 +48,12 @@
[eva] Done for function use_array
[eva] Recording results for main
[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}
[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 463ecd82baa00bef9d69d4a929427c293e46f394..a0c837faa9e45d2e9593b57280248b8b6eab5d90 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -128,6 +128,9 @@
[eva] computing for function gp <- main.
Called from origin.i:100.
[eva] using specification for function gp
+[eva:garbled-mix:assigns] origin.i:100:
+ The specification of function gp has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function gp
[eva:alarm] origin.i:101: Warning: out of bounds read. assert \valid_read(pl);
[eva] computing for function origin_misalign_1 <- main.
@@ -194,6 +197,20 @@
locals {local1} escaping the scope of local_escape_1 through esc4
[eva] Recording results for main
[eva] Done for function main
+[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}
+ origin.i:54: misaligned read of addresses
+ (read 3 times, propagated 1 times) garbled mix of &{a; b}
+ origin.i:14: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{ta1}
+ origin.i:25: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{ta3}
+ origin.i:100: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpp}
+ origin.i:48: misaligned read of addresses
+ (read 2 times, propagated 1 times) 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 23f2017157dd55ca36d768e50a104ca4b1bff071..4ca39e2f9666e88e958c97026512fbabd8a99cb5 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -74,6 +74,10 @@
because of arithmetic operation on addresses.
[eva] Recording results for origin
[eva] Done for function origin
+[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}
[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 bae921f2c83017e3d0a579fd5e57968d107db2cc..e949e737f124893354288c4ed3865a65d6396b74 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -94,6 +94,12 @@
pointer downcast. assert (unsigned int)(&vg) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
+[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}
+ period.c:53: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) 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 fd044aab639e3557a18f31a7ca6e5c4194ca3689..cb1dcc89815e6b7e167b7eb1a22971dcd955bda1 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -226,6 +226,9 @@
Analysis of function escaping_stack is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function escaping_stack
+[eva:garbled-mix:assigns] recursion.c:311:
+ The specification of function escaping_stack
+ has generated a garbled mix of addresses for assigns clause p.
[eva:alarm] recursion.c:313: Warning: out of bounds write. assert \valid(p);
[eva] recursion.c:314: Frama_C_show_each_1_2: {5}
[eva:locals-escaping] recursion.c:312: Warning:
@@ -236,6 +239,10 @@
Analysis of function decr is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function decr
+[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]}
[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 f74f2e91178601fd3731ee7c6db79b7e5c836b99..826021d49273bf80cfb3f3e201cd0fa2cc3507dc 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -145,6 +145,9 @@
[eva] computing for function garbled_mix <- main12 <- main.
Called from reduce_by_valid.i:272.
[eva] using specification for function garbled_mix
+[eva:garbled-mix:assigns] reduce_by_valid.i:272:
+ The specification of function garbled_mix
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function garbled_mix
[eva] reduce_by_valid.i:273:
Frama_C_show_each_gm:
@@ -167,12 +170,19 @@
out of bounds write. assert \valid(r);
[eva] computing for function garbled_mix <- main12 <- main.
Called from reduce_by_valid.i:290.
+[eva:garbled-mix:assigns] reduce_by_valid.i:290:
+ The specification of function garbled_mix
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function garbled_mix
[eva:alarm] reduce_by_valid.i:291: Warning: assertion got status unknown.
[eva] Recording results for main12
[eva] Done for function main12
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 0303ded6de4929bc22a0eae3ef2230863830238f..38218467e1391e87dd16adb079beca1594aa854e 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -61,6 +61,10 @@
unsigned overflow. assert 2U << 31 ≤ 4294967295;
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 2caaba30888d19cb802a92693305b2cb39762f6a..cf118f59bd758f7162dbcf25ddf0b285625eaa62 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -51,6 +51,10 @@
assert (long)r + (long)((long)((char *)t) << 8) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 9efb1b55c2d57c801e5e056dee0d78d42f817408..aa6a36837e24f63aa3c3f9e895594f1743c78872 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -46,6 +46,10 @@
[eva] Done for function f
[eva] Recording results for main
[eva] Done for function main
+[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}
[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 49e0e8774567b880a14053405a6e14e7c690d7b5..2b3a7d3e4a6bb9f37aa3a50764303572b75e81ae 100644
--- a/tests/value/oracle/va_list2.0.res.oracle
+++ b/tests/value/oracle/va_list2.0.res.oracle
@@ -36,6 +36,10 @@
{{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 24 times, propagated 10 times)
+ garbled mix of &{S_0_S___va_params; S_1_S___va_params}
[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_apron/backward_add_ptr.res.oracle b/tests/value/oracle_apron/backward_add_ptr.res.oracle
index ef19a912e467e231b3a3b3f3b80a52bb43737247..04bf26aed2a3d76fb3e5f7a704d63846dbaab183 100644
--- a/tests/value/oracle_apron/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_apron/backward_add_ptr.res.oracle
@@ -27,6 +27,6 @@
> [eva] Recording results for gm
> [eva] Done for function gm
154c166
-< (propagated 20 times, read 86 times) garbled mix of bases {a; b; a; b; c}
+< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
---
-> (propagated 28 times, read 90 times) garbled mix of bases {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 3829c4158e264ac75da7160ef40f37f47f4f8a8a..e39bbda029892bd78f7dccf1f133ee3e51428468 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]
-774c761
+778c765
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-777c764
+781c768
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
-813c800
+817c804
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 1f9878419ed0c405b36107f63d9e73f56b23b438..4527d4b279a58e63549f59ca9aef3f2765335771 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -5,32 +5,32 @@
< 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.
-144,147c138,139
-< (propagated 1 times, read 1 times) garbled mix of bases {p1}
-< addition.i:61: misaligned read of addresses
-< (propagated 1 times, read 1 times) garbled mix of bases {p1}
+141c135,139
< [scope:rm_asserts] removing 9 assertion(s)
---
-> (propagated 2 times, read 2 times) garbled mix of bases {p1}
+> [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}
> [scope:rm_asserts] removing 7 assertion(s)
-169c161
+163c161
< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
---
> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
-363,366d354
+357,360d354
< [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;
-375,378c363,364
-< (propagated 1 times, read 1 times) garbled mix of bases {p1}
-< addition.i:61: misaligned read of addresses
-< (propagated 1 times, read 1 times) garbled mix of bases {p1}
+366c360,364
< [scope:rm_asserts] removing 9 assertion(s)
---
-> (propagated 2 times, read 2 times) garbled mix of bases {p1}
+> [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}
> [scope:rm_asserts] removing 7 assertion(s)
-401c387
+389c387
< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
---
> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/arith_pointer.res.oracle b/tests/value/oracle_equality/arith_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e8d12d536a5435ae4567640619599a9d10b2e3ab
--- /dev/null
+++ b/tests/value/oracle_equality/arith_pointer.res.oracle
@@ -0,0 +1,8 @@
+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 38834abac9b8f039c5f0b3972dcb5d0f4e393e21..1b7ff53fec0b3b7db573cd6fc15fa8834ae8b229 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -24,6 +24,6 @@
> [eva] Recording results for gm
> [eva] Done for function gm
154c163
-< (propagated 20 times, read 86 times) garbled mix of bases {a; b; a; b; c}
+< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
---
-> (propagated 26 times, read 94 times) garbled mix of bases {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 46eace6fb725925449aeaf5c01f6ed18b2bd7a09..cfff35a117cceb9cdbac66aca878b2a19735854b 100644
--- a/tests/value/oracle_equality/bitfield.res.oracle
+++ b/tests/value/oracle_equality/bitfield.res.oracle
@@ -1,4 +1,8 @@
-134a135,137
+137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {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 0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 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 @@
-60c60
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-73c73
+79c79
< 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 0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 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 @@
-60c60
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-73c73
+79c79
< 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
new file mode 100644
index 0000000000000000000000000000000000000000..edf1bab4ce0f782dcf8cacb94936e89dd482ddbb
--- /dev/null
+++ b/tests/value/oracle_equality/context_free.res.oracle
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..a5fdd6006f01b6a3c868dca147b94ac07083a5ae
--- /dev/null
+++ b/tests/value/oracle_equality/empty_struct.6.res.oracle
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..1375772daf32d94c39da70a45a329a0af7e75df1
--- /dev/null
+++ b/tests/value/oracle_equality/gauges.res.oracle
@@ -0,0 +1,4 @@
+716c716
+< (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/library.res.oracle b/tests/value/oracle_equality/library.res.oracle
index 7ce2a4b0636c541b94a46f6ac3100e7660b079b8..60b76d8270d110e07713fc18e2042192a380e59e 100644
--- a/tests/value/oracle_equality/library.res.oracle
+++ b/tests/value/oracle_equality/library.res.oracle
@@ -1,4 +1,4 @@
-118,121d117
+124,127d123
< [eva:alarm] library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] library.i:44: Warning:
diff --git a/tests/value/oracle_equality/origin.0.res.oracle b/tests/value/oracle_equality/origin.0.res.oracle
index abe35687d18afa5ad7b79629a2d8594868b20ce1..a12449e315cdcbf000a4adcafec176f044d53066 100644
--- a/tests/value/oracle_equality/origin.0.res.oracle
+++ b/tests/value/oracle_equality/origin.0.res.oracle
@@ -1,9 +1,9 @@
-229,230c229
+246,247c246
< 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} }}
-264,265c263
+281,282c280
< 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 72c7991e2b3468da18583defce107fc497b4bb5a..657c13125d1d186b4e4b752cd479fb28e639a08b 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -4,5 +4,7 @@
< [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);
-97d91
+101,103d95
+< period.c:53: arithmetic operation on addresses
+< (read 2 times, propagated 1 times) 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
new file mode 100644
index 0000000000000000000000000000000000000000..2907faaa45d2cec4207024217ed66cf9699b41f8
--- /dev/null
+++ b/tests/value/oracle_equality/va_list2.0.res.oracle
@@ -0,0 +1,4 @@
+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 c47829e652e4b743152bbfca46d27650bab2fc3e..e84586701d0d94c7fe0b6eeef82d99fb3522fe2c 100644
--- a/tests/value/oracle_gauges/bitfield.res.oracle
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -1,4 +1,4 @@
-134a135,149
+137a138,152
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
@@ -14,3 +14,7 @@
> [eva] bitfield.i:73:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {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 1c645040cca978977f74a4d24ffac408484a6416..9d4462e029b227ddad11d18dc38dee160fab8cff 100644
--- a/tests/value/oracle_gauges/gauges.res.oracle
+++ b/tests/value/oracle_gauges/gauges.res.oracle
@@ -261,48 +261,52 @@
708a827,828
> [eva] gauges.c:343: Call to builtin malloc
> [eva] gauges.c:343: Call to builtin malloc
-761,762c881,882
+716c836
+< (read 14 times, propagated 12 times) garbled mix of &{x; y}
+---
+> (read 12 times, propagated 11 times) garbled mix of &{x; y}
+765,766c885,886
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
-774c894
+778c898
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-780c900
+784c904
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-786c906
+790c910
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-806c926
+810c930
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-808c928
+812c932
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-813c933
+817c937
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-824,825c944,946
+828,829c948,950
< [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] }}
-836c957
+840c961
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-841,845c962
+845,849c966
< n ∈ {0}
< arr[0] ∈ {0}
< [1] ∈ {-1}
@@ -310,19 +314,19 @@
< p ∈ {{ &arr + [12..--],0%4 }}
---
> NON TERMINATING FUNCTION
-948a1066
+952a1070
> [from] Non-terminating function main8_aux (no dependencies)
-971,972c1089,1090
+975,976c1093,1094
< 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]
-1016c1134
+1020c1138
< NO EFFECTS
---
> NON TERMINATING - NO EFFECTS
-1050c1168
+1054c1172
< 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 80fc106a63e0bc09c6ccf89c3f85ddb2cca12acd..70defd3cb22fe585b3ac25d1cbc4a5509d95456b 100644
--- a/tests/value/oracle_gauges/va_list2.0.res.oracle
+++ b/tests/value/oracle_gauges/va_list2.0.res.oracle
@@ -11,3 +11,7 @@
> [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 46eace6fb725925449aeaf5c01f6ed18b2bd7a09..cfff35a117cceb9cdbac66aca878b2a19735854b 100644
--- a/tests/value/oracle_octagon/bitfield.res.oracle
+++ b/tests/value/oracle_octagon/bitfield.res.oracle
@@ -1,4 +1,8 @@
-134a135,137
+137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {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 5b5cc28292675e05f4c652053a6c451c8d8744d1..1b2c6b235548585fb2d4218526d8c76fbed82258 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;
-763c756
+767c760
< numNonZero ∈ [-2147483648..8]
---
> numNonZero ∈ {-1}
-774c767
+778c771
< 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 0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 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 @@
-60c60
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-73c73
+79c79
< 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 0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 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 @@
-60c60
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-73c73
+79c79
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/library.res.oracle b/tests/value/oracle_symblocs/library.res.oracle
index 7ce2a4b0636c541b94a46f6ac3100e7660b079b8..60b76d8270d110e07713fc18e2042192a380e59e 100644
--- a/tests/value/oracle_symblocs/library.res.oracle
+++ b/tests/value/oracle_symblocs/library.res.oracle
@@ -1,4 +1,4 @@
-118,121d117
+124,127d123
< [eva:alarm] library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] library.i:44: Warning: