From 329e84d0937ee4b9fdf44e6ce80a7d6044fad8f2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Mar 2022 10:31:59 +0100
Subject: [PATCH] [wp/tests] introduce and use macros for sessions
---
src/plugins/wp/tests/test_config | 2 ++
src/plugins/wp/tests/test_config_qualif | 4 +++-
src/plugins/wp/tests/wp_eva/test_config_qualif | 2 +-
src/plugins/wp/tests/wp_gallery/binary-multiplication.c | 2 +-
src/plugins/wp/tests/wp_plugin/bitmask0x8000.i | 2 +-
src/plugins/wp/tests/wp_plugin/unroll.i | 2 +-
src/plugins/wp/tests/wp_plugin/unsigned.i | 2 +-
src/plugins/wp/tests/wp_tip/clear.i | 2 +-
src/plugins/wp/tests/wp_tip/induction.i | 6 +++---
src/plugins/wp/tests/wp_tip/induction_typing.i | 2 +-
src/plugins/wp/tests/wp_tip/modmask.i | 4 ++--
src/plugins/wp/tests/wp_tip/overflow.i | 2 +-
src/plugins/wp/tests/wp_tip/split.i | 2 +-
src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i | 2 +-
src/plugins/wp/tests/wp_tip/unroll.i | 2 +-
15 files changed, 21 insertions(+), 17 deletions(-)
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index da153c620d0..1c78f06e11e 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,3 +1,5 @@
PLUGIN: wp
+MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
+MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 2aa80fbe044..895b3f4d8bf 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,5 @@
PLUGIN: wp
-CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ -wp-cache-env -wp-cache replay @PTEST_FILE@
+MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
+MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
+CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@
OPT:
diff --git a/src/plugins/wp/tests/wp_eva/test_config_qualif b/src/plugins/wp/tests/wp_eva/test_config_qualif
index b4317853add..b9d5bf904c0 100644
--- a/src/plugins/wp/tests/wp_eva/test_config_qualif
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -1,3 +1,3 @@
PLUGIN: @PTEST_PLUGIN@,eva,scope,inout,reduc
-CMD: @frama-c@ -no-autoload-plugins -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ -wp-cache-env -wp-cache replay @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@
OPT:
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index 136dd578987..c365c6f4482 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack
+ OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@
*/
// The use '-wp-prover=z3,why3:alt-ergo' or using Alt-Ergo 2.3.0 gives better results.
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
index 42bfc7805cc..e2e5cf5fba3 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -wp-prover script,alt-ergo
+ OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/
typedef unsigned short ushort;
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index c1b7cc375bf..021ceb05d91 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script
+ OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script @USING_WP_SESSION@
*/
enum {Max = 16};
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i
index 95dcaeab725..a4075988005 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.i
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.i
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -wp-prover script
+ OPT: -wp-prover script @USING_WP_SESSION@
*/
/*@
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
index f1b443f2744..c4d1b5f5376 100644
--- a/src/plugins/wp/tests/wp_tip/clear.i
+++ b/src/plugins/wp/tests/wp_tip/clear.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i
index bf90bab1931..df4e3fa378d 100644
--- a/src/plugins/wp/tests/wp_tip/induction.i
+++ b/src/plugins/wp/tests/wp_tip/induction.i
@@ -4,11 +4,11 @@
/* run.config_qualif
- OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
- OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
- OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
*/
// Script 0: induction on f(x) => success
diff --git a/src/plugins/wp/tests/wp_tip/induction_typing.i b/src/plugins/wp/tests/wp_tip/induction_typing.i
index 4c175309ccb..4f9b82169e6 100644
--- a/src/plugins/wp/tests/wp_tip/induction_typing.i
+++ b/src/plugins/wp/tests/wp_tip/induction_typing.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,script -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i
index 1e9983dd51e..4da4f942609 100644
--- a/src/plugins/wp/tests/wp_tip/modmask.i
+++ b/src/plugins/wp/tests/wp_tip/modmask.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/overflow.i b/src/plugins/wp/tests/wp_tip/overflow.i
index 13cd10c72d5..34298d91ee6 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.i
+++ b/src/plugins/wp/tests/wp_tip/overflow.i
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
*/
typedef unsigned int uint;
diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i
index 60cc76525e9..27c531dbae2 100644
--- a/src/plugins/wp/tests/wp_tip/split.i
+++ b/src/plugins/wp/tests/wp_tip/split.i
@@ -1,6 +1,6 @@
/* run.config
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
index 6ee79e67684..fd890b44fd3 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -5,7 +5,7 @@
/* run.config_qualif
SCRIPT: TacNOP
- OPT: -wp -wp-par 1 -wp-prover script
+ OPT: -wp -wp-par 1 -wp-prover script @USING_WP_SESSION@
*/
diff --git a/src/plugins/wp/tests/wp_tip/unroll.i b/src/plugins/wp/tests/wp_tip/unroll.i
index 5019c19200a..df1151d0372 100644
--- a/src/plugins/wp/tests/wp_tip/unroll.i
+++ b/src/plugins/wp/tests/wp_tip/unroll.i
@@ -4,7 +4,7 @@
/* run.config_qualif
- OPT: -wp-prover script,none
+ OPT: -wp-prover script,none @USING_WP_SESSION@
*/
/*@
--
GitLab