[wp/tests] introduce and use macros for sessions

src/plugins/wp/tests/test_config

 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:

src/plugins/wp/tests/test_config_qualif

 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:

src/plugins/wp/tests/wp_eva/test_config_qualif

 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:

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.

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;

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};

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@
 */
 
 /*@

src/plugins/wp/tests/wp_tip/clear.i

 /* 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:

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

src/plugins/wp/tests/wp_tip/induction_typing.i

 /* 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:

src/plugins/wp/tests/wp_tip/modmask.i

 /* 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:

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;

src/plugins/wp/tests/wp_tip/split.i

 /* 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:

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@
 */
 
 

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@
  */
 
 /*@