From c4c96feda85946feab96bfd1c123cd7b775db982 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Mar 2022 11:30:59 +0100
Subject: [PATCH] [wp] Use PTEST_DIR for sessions
---
src/plugins/wp/tests/test_config_qualif | 2 +-
src/plugins/wp/tests/wp_eva/test_config_qualif | 2 +-
src/plugins/wp/tests/wp_tip/clear.i | 2 +-
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/split.i | 2 +-
src/plugins/wp/tests/wp_typed/user_init.i | 2 +-
7 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index ef26b5e0741..98fc19b9f70 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,3 @@
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 @PTEST_SUITE_DIR@/../qualif.report -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ -wp-cache-env -wp-cache replay @PTEST_FILE@
+CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report @PTEST_SUITE_DIR@/../qualif.report -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ -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 5cc6f72566c..797af6dc949 100644
--- a/src/plugins/wp/tests/wp_eva/test_config_qualif
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -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-report tests/qualif.report -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -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-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@
OPT:
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
index fda3206942b..659d31a9359 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,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/induction_typing.i b/src/plugins/wp/tests/wp_tip/induction_typing.i
index 9e5a8bc2131..869dd8f2282 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,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.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 686c9443d3d..eb9501996b8 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,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i
index 6e69150d4b4..80e7fb305f2 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,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
*/
/* run.config_qualif
DONTRUN:
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index 251dcd36298..6bda4f9640b 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- EXECNOW: rm -rf @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session/script
+ EXECNOW: rm -rf @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session/script
OPT: -wp-prop=-lack,-tactic
OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,alt-ergo
OPT: -wp-prop=lack
--
GitLab