[Eva] Enables all garbled mix messages by default.

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.

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 ||

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"

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 ∈

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

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,

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}

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.

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] ∈

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 ∈ [--..--]

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 }}

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.

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}

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.

tests/builtins/oracle_gauges/linked_list.1.res.oracle

-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

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.

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.

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}

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}

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}