From 5766f0311dba78297ae5c96ff6f10c94e83c5a5c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Oct 2024 10:11:05 +0200
Subject: [PATCH] [Eva] Removes a run with RTE of the div.i test.
---
tests/value/div.i | 6 +-
tests/value/oracle/div.1.res.oracle | 124 ------------------
.../{div.0.res.oracle => div.res.oracle} | 0
3 files changed, 3 insertions(+), 127 deletions(-)
delete mode 100644 tests/value/oracle/div.1.res.oracle
rename tests/value/oracle/{div.0.res.oracle => div.res.oracle} (100%)
diff --git a/tests/value/div.i b/tests/value/div.i
index 55857e727f9..a57ddb2084a 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,8 +1,8 @@
/* run.config*
- STDOPT: #"-eva-remove-redundant-alarms"
- PLUGIN: @PTEST_PLUGIN@ rtegen
- OPT: -machdep x86_32 @RTE_TEST@ -then -eva @EVA_CONFIG@
+ STDOPT: #""
*/
+
+
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
int t[5]={1,2,3};
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
deleted file mode 100644
index 6cc6efc9056..00000000000
--- a/tests/value/oracle/div.1.res.oracle
+++ /dev/null
@@ -1,124 +0,0 @@
-[kernel] Parsing div.i (no preprocessing)
-[rte:annot] annotating function main
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- X ∈ {0}
- Y ∈ {0}
- Z1 ∈ {0}
- Z2 ∈ {0}
- T ∈ {0}
- U1 ∈ {0}
- U2 ∈ {0}
- V ∈ {0}
- W1 ∈ {0}
- W2 ∈ {0}
- a ∈ {0}
- b ∈ {0}
- d1 ∈ {0}
- d2 ∈ {0}
- d0 ∈ {0}
- e ∈ {0}
- t[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- [3..4] ∈ {0}
- p ∈ {0}
-[eva:alarm] div.i:14: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:14: Warning: signed overflow. assert c + 1 ≤ 2147483647;
-[eva] div.i:16: assertion 'rte,signed_overflow' got status valid.
-[eva:alarm] div.i:17: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:17: Warning: signed overflow. assert c + 2 ≤ 2147483647;
-[eva] div.i:17: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:14: starting to merge loop iterations
-[eva:alarm] div.i:17: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:17: Warning: signed overflow. assert -2147483648 ≤ X - 1;
-[eva:alarm] div.i:16: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:16: Warning: signed overflow. assert X + 1 ≤ 2147483647;
-[eva] div.i:22: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:25: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:28: assertion 'rte,signed_overflow' got status valid.
-[eva:alarm] div.i:32: Warning:
- assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:32: Warning: division by zero. assert Z2 ≢ 0;
-[eva:alarm] div.i:33: Warning:
- assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:33: Warning:
- assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:33: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:33: Warning: division by zero. assert Z2 ≢ 0;
-[eva:alarm] div.i:33: Warning:
- pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
-[eva:alarm] div.i:33: Warning:
- signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
-[eva:garbled-mix:write] div.i:33:
- Assigning imprecise value to b because of arithmetic operation on addresses.
-[eva:alarm] div.i:34: Warning:
- assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:34: Warning:
- assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:34: Warning:
- pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
-[eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
-[eva:garbled-mix:write] div.i:34:
- Assigning imprecise value to d2 because of arithmetic operation on addresses.
-[eva:alarm] div.i:35: Warning:
- assertion 'rte,pointer_downcast' got status unknown.
-[eva] div.i:35: assertion 'rte,division_by_zero' got status valid.
-[eva:alarm] div.i:35: Warning:
- pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:35:
- Assigning imprecise value to d1 because of arithmetic operation on addresses.
-[eva:alarm] div.i:36: Warning:
- assertion 'rte,pointer_downcast' got status unknown.
-[eva] div.i:36: assertion 'rte,division_by_zero' got status valid.
-[eva:alarm] div.i:36: Warning:
- pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:36:
- Assigning imprecise value to d0 because of arithmetic operation on addresses.
-[eva:alarm] div.i:37: Warning:
- assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:37: Warning:
- assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:37: Warning:
- pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:37: Warning:
- signed overflow. assert -2147483648 ≤ -((int)(&X));
-[eva:alarm] div.i:37: Warning:
- signed overflow. assert -((int)(&X)) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:37:
- Assigning imprecise value to e because of arithmetic operation on addresses.
-[eva] Recording results for main
-[eva] Done for function main
-[eva] div.i:22: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:25: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:28: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:35: assertion 'rte,division_by_zero' got final status valid.
-[eva] div.i:36: assertion 'rte,division_by_zero' got final status valid.
-[scope:rm_asserts] removing 2 assertion(s)
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- X ∈ [--..--]
- Y ∈ [-126..333],9%27
- Z1 ∈ [-42..111],3%9
- Z2 ∈ [-25..66]
- T ∈ [34..493],7%27
- U1 ∈ [11..164],2%9
- U2 ∈ [6..98]
- V ∈ [-125..334],10%27
- W1 ∈ [-41..111]
- W2 ∈ [-25..66]
- a ∈ [-40000..40000]
- b ∈ {{ garbled mix of &{Z2} (origin: Arithmetic {div.i:33}) }}
- d1 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:35}) }}
- d2 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:34}) }}
- d0 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:36}) }}
- e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
- p ∈ {{ &t[3] }}
- c ∈ [--..--]
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.res.oracle
similarity index 100%
rename from tests/value/oracle/div.0.res.oracle
rename to tests/value/oracle/div.res.oracle
--
GitLab