From ce1b5d311f745b930e95693c01ea9adb888f0a9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 15 Feb 2024 20:32:53 +0100
Subject: [PATCH] [Eva] Updates test oracles.
---
tests/value/oracle/addition.res.oracle | 34 -------------------
.../value/oracle/backward_add_ptr.res.oracle | 28 ++-------------
tests/value/oracle/join_misaligned.res.oracle | 4 ---
tests/value/oracle/struct3.res.oracle | 3 --
4 files changed, 3 insertions(+), 66 deletions(-)
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index bb68a90bfb7..cac259e96f2 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 aa5bb85d725..d55109dbd30 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 82adf0d093d..923f7c4aa5d 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 20c83c1fc97..2ab398ecfda 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:
--
GitLab