From d078323511f7212df5827b2b275a6cd7f52c9711 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 16 Feb 2024 12:41:05 +0100
Subject: [PATCH] [Eva] Enables all garbled mix messages by default.
---
.../tests/dive/oracle/exceptional.res.oracle | 4 +++
.../bts/oracle/issue-eacsl-145.res.oracle | 3 ++
src/plugins/eva/self.ml | 4 +--
.../sum_with_unspecified_sequence.res.oracle | 4 +++
.../tests/known/oracle/exec.res.oracle | 12 +++++++
.../tests/known/oracle/printf.res.oracle | 4 +++
.../oracle/printf_garbled_mix.res.oracle | 4 +++
tests/builtins/oracle/alloc.0.res.oracle | 4 +++
tests/builtins/oracle/alloc.1.res.oracle | 5 +++
.../oracle/imprecise-malloc-free.res.oracle | 4 +++
tests/builtins/oracle/imprecise.res.oracle | 8 +++++
.../builtins/oracle/linked_list.1.res.oracle | 4 +++
tests/builtins/oracle/strchr.res.oracle | 4 +++
.../oracle_equality/linked_list.1.res.oracle | 4 +--
.../oracle_gauges/linked_list.1.res.oracle | 2 +-
.../oracle_octagon/linked_list.1.res.oracle | 4 +--
.../oracle_symblocs/linked_list.1.res.oracle | 4 +--
tests/float/oracle/nonlin.0.res.oracle | 4 +++
tests/float/oracle/nonlin.1.res.oracle | 4 +++
tests/float/oracle/nonlin.2.res.oracle | 4 +++
tests/float/oracle/nonlin.3.res.oracle | 4 +++
tests/float/oracle/nonlin.4.res.oracle | 4 +++
tests/float/oracle/nonlin.5.res.oracle | 4 +++
tests/libc/oracle/pwd_h.res.oracle | 6 ++++
tests/libc/oracle/signal_h.res.oracle | 6 ++++
tests/libc/oracle/spawn_h.res.oracle | 8 +++++
tests/libc/oracle/unistd_h.0.res.oracle | 3 ++
tests/slicing/oracle/loops.10.res.oracle | 3 ++
tests/slicing/oracle/loops.19.res.oracle | 3 ++
tests/slicing/oracle/loops.20.res.oracle | 3 ++
tests/slicing/oracle/loops.21.res.oracle | 3 ++
tests/slicing/oracle/loops.22.res.oracle | 3 ++
tests/slicing/oracle/loops.23.res.oracle | 3 ++
tests/slicing/oracle/loops.8.res.oracle | 3 ++
tests/slicing/oracle/loops.9.res.oracle | 3 ++
tests/value/oracle/arith_pointer.res.oracle | 14 ++++++++
.../oracle/assign-leaf-indirect.res.oracle | 3 ++
tests/value/oracle/assigns_from.res.oracle | 3 ++
tests/value/oracle/behaviors1.res.oracle | 12 +++++++
tests/value/oracle/bitfield.res.oracle | 7 ++++
.../value/oracle/bitwise_pointer.0.res.oracle | 6 ++++
.../value/oracle/bitwise_pointer.1.res.oracle | 6 ++++
tests/value/oracle/context_free.res.oracle | 4 +++
tests/value/oracle/degeneration2.res.oracle | 4 +++
tests/value/oracle/empty_struct.6.res.oracle | 7 ++++
tests/value/oracle/from_call.0.res.oracle | 3 ++
tests/value/oracle/from_call.1.res.oracle | 3 ++
tests/value/oracle/gauges.res.oracle | 4 +++
.../oracle/imprecise_invalid_write.res.oracle | 6 ++++
tests/value/oracle/initialized.res.oracle | 4 +++
tests/value/oracle/inout_proto.res.oracle | 3 ++
tests/value/oracle/leaf.res.oracle | 24 ++++++++++++++
tests/value/oracle/leaf2.res.oracle | 7 ++++
tests/value/oracle/library.res.oracle | 17 ++++++++++
tests/value/oracle/logic.res.oracle | 7 ++++
.../oracle/multidim-relations.res.oracle | 6 ++++
tests/value/oracle/origin.0.res.oracle | 17 ++++++++++
tests/value/oracle/origin.1.res.oracle | 4 +++
tests/value/oracle/period.res.oracle | 6 ++++
tests/value/oracle/recursion.0.res.oracle | 7 ++++
tests/value/oracle/reduce_by_valid.res.oracle | 10 ++++++
tests/value/oracle/shift.0.res.oracle | 4 +++
tests/value/oracle/shift.1.res.oracle | 4 +++
tests/value/oracle/sizeof.res.oracle | 4 +++
tests/value/oracle/va_list2.0.res.oracle | 4 +++
.../oracle_apron/backward_add_ptr.res.oracle | 4 +--
tests/value/oracle_apron/gauges.res.oracle | 6 ++--
.../value/oracle_bitwise/addition.res.oracle | 0
.../bitwise_pointer.0.res.oracle | 0
.../bitwise_pointer.1.res.oracle | 0
.../oracle_bitwise/logic_ptr_cast.res.oracle | 0
.../value/oracle_equality/addition.res.oracle | 26 +++++++--------
.../oracle_equality/arith_pointer.res.oracle | 8 +++++
.../backward_add_ptr.res.oracle | 4 +--
.../value/oracle_equality/bitfield.res.oracle | 6 +++-
.../bitwise_pointer.0.res.oracle | 4 +--
.../bitwise_pointer.1.res.oracle | 4 +--
.../oracle_equality/context_free.res.oracle | 4 +++
.../oracle_equality/empty_struct.6.res.oracle | 4 +++
tests/value/oracle_equality/gauges.res.oracle | 4 +++
.../value/oracle_equality/library.res.oracle | 2 +-
.../value/oracle_equality/origin.0.res.oracle | 4 +--
tests/value/oracle_equality/period.res.oracle | 4 ++-
.../oracle_equality/va_list2.0.res.oracle | 4 +++
tests/value/oracle_gauges/bitfield.res.oracle | 6 +++-
tests/value/oracle_gauges/gauges.res.oracle | 32 +++++++++++--------
.../value/oracle_gauges/va_list2.0.res.oracle | 4 +++
.../value/oracle_octagon/bitfield.res.oracle | 6 +++-
tests/value/oracle_octagon/gauges.res.oracle | 4 +--
.../bitwise_pointer.0.res.oracle | 4 +--
.../bitwise_pointer.1.res.oracle | 4 +--
.../value/oracle_symblocs/library.res.oracle | 2 +-
92 files changed, 448 insertions(+), 61 deletions(-)
delete mode 100644 tests/value/oracle_bitwise/addition.res.oracle
delete mode 100644 tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
delete mode 100644 tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
delete mode 100644 tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
create mode 100644 tests/value/oracle_equality/arith_pointer.res.oracle
create mode 100644 tests/value/oracle_equality/context_free.res.oracle
create mode 100644 tests/value/oracle_equality/empty_struct.6.res.oracle
create mode 100644 tests/value/oracle_equality/gauges.res.oracle
create mode 100644 tests/value/oracle_equality/va_list2.0.res.oracle
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index 47e5fcec857..ae50bf359dc 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 44a3cdfd58d..201d2b2a599 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 88f3fdf2c69..d1c33a8a5ee 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 d8fbec93f6a..0597fca78db 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 74ea04f2c8f..335dfe32f04 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 efb382209eb..7b945647be0 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 55f26985dfe..2db3d363037 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 7ce75e72f21..684b949a466 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 7633c770d71..77bfca7bbb7 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 7134efd0323..4cd01a4b78e 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 ec7cb60e6e2..1ad813d673e 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 16a5a8ec3b5..c97ebeb2a70 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 ffbebfd90e0..e1298461c03 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 dc1c07fbca0..08a077ea283 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 ec6dff88c11..b4dd8f6901b 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 4083e687dd3..166d64faad7 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 4083e687dd3..166d64faad7 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 04ffb0d077b..043c52aa669 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 54cd152e82f..b69461ed024 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 9ae60320eb1..05b14b3983b 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 17b03c98f92..24ccbef205c 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 33877fa4e08..a0f41891c24 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 66c509fd9b8..25cd26ba1ee 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 6cdda1a2be9..5dedb215f1a 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 1b2258ac3dd..fe4f9414bf7 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 4b4c978087e..08866e9f1aa 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 24a810167ef..46a982f0c80 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 8b074bf06ab..7ba1874acea 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 34457cfad25..0998264ade1 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 27d8cdb8355..6e18bd872d2 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 9adf543884b..8636ad07b17 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 7d41e9a40cd..3313fbc32d9 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 24eb43a90cb..ae8f97a78fc 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 3c7880c3af1..f1d9bbd8669 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 abc0b21b556..a2caa35921c 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 d8c8908c4b6..2261d0849e3 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 d1632315bcb..4d4a939a92b 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 002087f31ba..55b41ae8a07 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 c434339fdec..6266ee5cf35 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 3b980d881cf..3751001cbba 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 aa3a3f4a6a2..6b52884383a 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 aa3a3f4a6a2..6b52884383a 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 ffee5073aff..ba68025f931 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 de456405cd9..e792578b81a 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 88263f19b58..cf2ce4f7e50 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 88c6c5d8c6d..f3377d39ae6 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 560d21d929a..18901931cee 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 ce2c46bcca8..4b7f0372dd0 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 3b45112de2a..49172ffd8d9 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 1e822fd04fa..150e3f18242 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 77fcb77f701..d96ee3689cb 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 d966184b444..865b2bc8486 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 5de89a4124f..c03b05b96d4 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 01756f25fda..992d56c788e 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 cc514176b48..77e8322bc7e 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 e7f1d9da7ac..aa7000e536d 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 463ecd82baa..a0c837faa9e 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 23f2017157d..4ca39e2f966 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 bae921f2c83..e949e737f12 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 fd044aab639..cb1dcc89815 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 f74f2e91178..826021d4927 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 0303ded6de4..38218467e13 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 2caaba30888..cf118f59bd7 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 9efb1b55c2d..aa6a36837e2 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 49e0e877456..2b3a7d3e4a6 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 ef19a912e46..04bf26aed2a 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 3829c4158e2..e39bbda0298 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 e69de29bb2d..00000000000
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 e69de29bb2d..00000000000
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 e69de29bb2d..00000000000
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 e69de29bb2d..00000000000
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 1f9878419ed..4527d4b279a 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 00000000000..e8d12d536a5
--- /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 38834abac9b..1b7ff53fec0 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 46eace6fb72..cfff35a117c 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 0b286b81268..688b8e07ea0 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 0b286b81268..688b8e07ea0 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 00000000000..edf1bab4ce0
--- /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 00000000000..a5fdd6006f0
--- /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 00000000000..1375772daf3
--- /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 7ce2a4b0636..60b76d8270d 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 abe35687d18..a12449e315c 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 72c7991e2b3..657c13125d1 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 00000000000..2907faaa45d
--- /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 c47829e652e..e84586701d0 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 1c645040cca..9d4462e029b 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 80fc106a63e..70defd3cb22 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 46eace6fb72..cfff35a117c 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 5b5cc282926..1b2c6b23554 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 0b286b81268..688b8e07ea0 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 0b286b81268..688b8e07ea0 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 7ce2a4b0636..60b76d8270d 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:
--
GitLab