From 44c1e708e5467a9ad4603c57657aa49026ddcd6c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 14 Jan 2022 22:19:17 +0100
Subject: [PATCH] [Eva] Fixes some tests.
---
tests/value/memexec.c | 4 ++--
tests/value/oracle/summary.4.res.oracle | 6 +++---
tests/value/summary.i | 4 ++--
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/tests/value/memexec.c b/tests/value/memexec.c
index bb6bb912db9..e87602726a1 100644
--- a/tests/value/memexec.c
+++ b/tests/value/memexec.c
@@ -1,7 +1,7 @@
/* run.config*
- STDOPT: +"-rte-select fbug @RTE_TEST@ -then -eva"
+ PLUGIN: @PTEST_PLUGIN@ rtegen
+ STDOPT: #"-machdep x86_32 -rte-select fbug @RTE_TEST@ -then -eva"
*/
-
int x1, y1, z1, z2; volatile int c, nondet;
void f11() {
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 6faede6c061..81eb2443521 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -1,5 +1,3 @@
-[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
- Please use -eva-slevel instead.
[kernel] Parsing summary.i (no preprocessing)
[rte:annot] annotating function alarms
[rte:annot] annotating function bottom
@@ -8,6 +6,8 @@
[rte:annot] annotating function logic
[rte:annot] annotating function main
[rte:annot] annotating function minimal
+[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
+ Please use -eva-slevel instead.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -107,7 +107,7 @@
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 2 warnings
+ by the Frama-C kernel: 0 errors 3 warnings
----------------------------------------------------------------------------
18 alarms generated by the analysis:
3 invalid memory accesses
diff --git a/tests/value/summary.i b/tests/value/summary.i
index 718f105808a..3ef6022672e 100644
--- a/tests/value/summary.i
+++ b/tests/value/summary.i
@@ -3,8 +3,8 @@
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main main"
-PLUGIN: @PTEST_PLUGIN@ rtegen
- STDOPT: +"@RTE_TEST@ -eva-msg-key=summary -main main -slevel 0"
+ PLUGIN: @PTEST_PLUGIN@ rtegen
+ OPT: -machdep x86_32 @RTE_TEST@ -then @EVA_TEST@ -eva-msg-key=summary -main main -slevel 0
*/
/* Tests the summary on the smallest possible program. */
void minimalist ();
--
GitLab