From 942e9bbb8e910c36a93dbcff132a8d6ed287547d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Dec 2018 16:36:07 +0100
Subject: [PATCH] [Eva] Updates the memexec option in the tests.
---
tests/builtins/malloc-optimistic.c | 2 +-
tests/builtins/malloc_memexec.c | 2 +-
tests/idct/ieee_1180_1990.c | 2 +-
tests/value/logicdeps.i | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c
index 67dea08d8a9..bb1e66301f3 100644
--- a/tests/builtins/malloc-optimistic.c
+++ b/tests/builtins/malloc-optimistic.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -memexec-all"
+ STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -eva-memexec"
*/
//@ assigns \result \from \nothing;
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 73caf738d77..004e113f619 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -eva @VALUECONFIG@ -memexec-all -deps -inout -eva-mlevel 0
+ OPT: -eva @VALUECONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
*/
//@ assigns \result;
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index 4926fbb95a5..1f0f4325eeb 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -memexec-all -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
+ STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
*/
/* IEEE_1180_1990: a testbed for IDCT accuracy
* Copyright (C) 2001 Renaud Pacalet
diff --git a/tests/value/logicdeps.i b/tests/value/logicdeps.i
index 94e2e15754f..d9cb3cbed54 100644
--- a/tests/value/logicdeps.i
+++ b/tests/value/logicdeps.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-memexec-all -calldeps -no-deps -no-input -no-out -then -inout"
+ STDOPT: +"-eva-memexec -calldeps -no-deps -no-input -no-out -then -inout"
*/
int t[50];
--
GitLab