From ef2504adc366b80d33e30455834e2b2e2df77a11 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 17 Oct 2018 19:29:29 +0200
Subject: [PATCH] [tests] update options against kernel changes
---
src/plugins/e-acsl/tests/bts/test_config | 2 +-
src/plugins/e-acsl/tests/builtin/test_config | 2 +-
src/plugins/e-acsl/tests/format/test_config | 2 +-
src/plugins/e-acsl/tests/full-mmodel-only/test_config | 2 +-
src/plugins/e-acsl/tests/full-mmodel/test_config | 4 ++--
src/plugins/e-acsl/tests/gmp/test_config | 4 ++--
src/plugins/e-acsl/tests/runtime/test_config | 2 +-
src/plugins/e-acsl/tests/temporal/t_getenv.c | 2 +-
src/plugins/e-acsl/tests/temporal/test_config | 2 +-
9 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
index d7b9c838f9f..1fb42e2f912 100644
--- a/src/plugins/e-acsl/tests/bts/test_config
+++ b/src/plugins/e-acsl/tests/bts/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
+OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
diff --git a/src/plugins/e-acsl/tests/builtin/test_config b/src/plugins/e-acsl/tests/builtin/test_config
index 0a3bc2dc49d..d10e3bc47b5 100644
--- a/src/plugins/e-acsl/tests/builtin/test_config
+++ b/src/plugins/e-acsl/tests/builtin/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-replace-libc-functions -then-last -load-script tests/print.cmxs -print -ocode tests/builtin/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-replace-libc-functions -then-last -load-script tests/print.cmxs -print -ocode tests/builtin/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results
EXEC: ./scripts/testrun.sh @PTEST_NAME@ builtin "1" "--frama-c=@frama-c@ --full-mmodel --libc-replacements"
diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config
index 8f2dae04629..c42ada82ec5 100644
--- a/src/plugins/e-acsl/tests/format/test_config
+++ b/src/plugins/e-acsl/tests/format/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=-annot:missing-spec -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=annot:missing-spec=inactive -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results
EXEC: ./scripts/testrun.sh @PTEST_NAME@ format "1" "--frama-c=@frama-c@ --full-mmodel --validate-format-strings"
diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/test_config b/src/plugins/e-acsl/tests/full-mmodel-only/test_config
index d5f839c452f..3920419f522 100644
--- a/src/plugins/e-acsl/tests/full-mmodel-only/test_config
+++ b/src/plugins/e-acsl/tests/full-mmodel-only/test_config
@@ -1,3 +1,3 @@
EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel-only "1" "--frama-c=@frama-c@ --full-mmodel"
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
\ No newline at end of file
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config
index 31e1db413b1..dfe9f67a078 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/test_config
+++ b/src/plugins/e-acsl/tests/full-mmodel/test_config
@@ -1,5 +1,5 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results
EXEC: ./scripts/testrun.sh @PTEST_NAME@ full-mmodel "1" "--frama-c=@frama-c@ --full-mmodel"
LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -then-last -load-script tests/print.cmxs -print -ocode tests/full-mmodel/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
index 645d2c1fa60..5b2172b01dd 100644
--- a/src/plugins/e-acsl/tests/gmp/test_config
+++ b/src/plugins/e-acsl/tests/gmp/test_config
@@ -1,5 +1,5 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results -eva-no-alloc-returns-null
EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -eva -eva-no-print -eva-no-show-progress -no-results -eva-no-alloc-returns-null
diff --git a/src/plugins/e-acsl/tests/runtime/test_config b/src/plugins/e-acsl/tests/runtime/test_config
index b1256ec5a21..3d07f750042 100644
--- a/src/plugins/e-acsl/tests/runtime/test_config
+++ b/src/plugins/e-acsl/tests/runtime/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/runtime/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@"
diff --git a/src/plugins/e-acsl/tests/temporal/t_getenv.c b/src/plugins/e-acsl/tests/temporal/t_getenv.c
index 259c1b18ddc..41dfd454996 100644
--- a/src/plugins/e-acsl/tests/temporal/t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/t_getenv.c
@@ -1,6 +1,6 @@
/* run.config
COMMENT: Check temporal validity of environment string (via getenv function)
- STDOPT: #"-eva-warn-key=-libc:unsupported-spec"
+ STDOPT: #"-eva-warn-key=libc:unsupported-spec=inactive"
*/
#include <stdlib.h>
#include <errno.h>
diff --git a/src/plugins/e-acsl/tests/temporal/test_config b/src/plugins/e-acsl/tests/temporal/test_config
index 395b62c1735..c9b7be37341 100644
--- a/src/plugins/e-acsl/tests/temporal/test_config
+++ b/src/plugins/e-acsl/tests/temporal/test_config
@@ -1,3 +1,3 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-temporal-validity -then-last -load-script tests/print.cmxs -print -ocode tests/temporal/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 -value-warn-key="-alarm"
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-temporal-validity -then-last -load-script tests/print.cmxs -print -ocode tests/temporal/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0 -eva-warn-key="alarm=inactive"
EXEC: ./scripts/testrun.sh @PTEST_NAME@ temporal "" "--frama-c=@frama-c@ --full-mmodel --temporal"
--
GitLab