diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle index bb68a90bfb7a65ffac5bbbed34e7e8fa86d5bc50..cac259e96f2175dd68ab9ba81d78b1b0e2df7de3 100644 --- a/tests/value/oracle/addition.res.oracle +++ b/tests/value/oracle/addition.res.oracle @@ -148,23 +148,6 @@ [eva] addition.i:88: assertion got status valid. [eva] Recording results for main [eva] Done for function main -[eva:garbled-mix:summary] Warning: - Garbled mix generated during analysis: - {{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }} - {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }} - {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }} [scope:rm_asserts] removing 9 assertion(s) [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: @@ -390,23 +373,6 @@ [eva] addition.i:87: Frama_C_show_each_1: [-10..15] [eva] Recording results for main [eva] Done for function main -[eva:garbled-mix:summary] Warning: - Garbled mix generated during analysis: - {{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }} - {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }} - {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }} - {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }} - {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }} [scope:rm_asserts] removing 9 assertion(s) [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: diff --git a/tests/value/oracle/backward_add_ptr.res.oracle b/tests/value/oracle/backward_add_ptr.res.oracle index aa5bb85d7250e40cd2b703b4a4807dcc83115c30..d55109dbd308d126b923440c8325fa80ab08a693 100644 --- a/tests/value/oracle/backward_add_ptr.res.oracle +++ b/tests/value/oracle/backward_add_ptr.res.oracle @@ -182,31 +182,9 @@ [eva] Recording results for main [eva] Done for function main [eva:garbled-mix:summary] Warning: - Garbled mix generated during analysis: - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:25}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:25}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:32}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:32}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:38}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:38}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:54}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:54}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:60}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:60}) }} - {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:68}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:81}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:87}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:96}) }} - {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:106}) }} - {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }} - {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:115}) }} - {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:121}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:130}) }} - {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:136}) }} - {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }} - {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:68}) }} - {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:68}) }} + Origins of garbled mix generated during analysis: + backward_add_ptr.c:68: arithmetic operation on addresses + (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c} [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function gm: __retres ∈ diff --git a/tests/value/oracle/join_misaligned.res.oracle b/tests/value/oracle/join_misaligned.res.oracle index 82adf0d093dbffd8bfb9b2ca4928d6650ad4e8af..923f7c4aa5d06383052e0ed08a4ac10cfc406200 100644 --- a/tests/value/oracle/join_misaligned.res.oracle +++ b/tests/value/oracle/join_misaligned.res.oracle @@ -20,10 +20,6 @@ pointer downcast. assert (unsigned int)(&u) ≤ 2147483647; [eva] Recording results for main [eva] Done for function main -[eva:garbled-mix:summary] Warning: - Garbled mix generated during analysis: - {{ garbled mix of &{t} (origin: Merge {join_misaligned.i:42}) }} - {{ garbled mix of &{u} (origin: Merge {join_misaligned.i:42}) }} [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: t{[0]; [1][bits 0 to 15]} ∈ {0} diff --git a/tests/value/oracle/struct3.res.oracle b/tests/value/oracle/struct3.res.oracle index 20c83c1fc97b7e5983a55566c669ea7d3b98d68c..2ab398ecfda2225ff7f334606d192913e00d704a 100644 --- a/tests/value/oracle/struct3.res.oracle +++ b/tests/value/oracle/struct3.res.oracle @@ -28,9 +28,6 @@ The imprecision originates from Arithmetic {struct3.i:46} [eva] Recording results for main [eva] Done for function main -[eva:garbled-mix:summary] Warning: - Garbled mix generated during analysis: - {{ garbled mix of &{s1} (origin: Arithmetic {struct3.i:46}) }} [eva] struct3.i:42: assertion 'Eva,index_bound' got final status invalid. [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: