diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config index da153c620d01ac5748f1fb26e4d9998e24888f3a..1c78f06e11e80018180777668c123942cf82c868 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 2aa80fbe044ca20725302dc8453d234ec5bd1aaf..895b3f4d8bf4111e4f6df1692cdf3675fce834b5 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 b4317853adde06a160821af20f8605f2b2585797..b9d5bf904c05cb9b2bfb19a84d135b651b8cecf1 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 136dd5789872fc978cfb6cf4c4f92451b41c6512..c365c6f448277fca904f52231225bc5af90dc7b4 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 42bfc7805cc0513802f07a2531f98cb5fba93fb0..e2e5cf5fba38b6d8860003cd779ae364c30805a3 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 c1b7cc375bf401feaec0ff7ced12d1fc3a1481b1..021ceb05d916d53f2b67bce5c86c714481e51d4e 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 95dcaeab7254847bebcb1523ff3344d9285f43a7..a4075988005d6bb74ee68e849bcf67ae8789720f 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 f1b443f27449ce4f3a8e01ca68fc3ab71f6a1e8a..c4d1b5f53767129850bb885e4ca5eb6261a9d740 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 bf90bab193167ebe3beee9f9f15659eedeff7a95..df4e3fa378d1c13704c8af6e64803040b93b565f 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 4c175309ccb3f56ea269baeb7d8246256f2385e4..4f9b82169e695cd8280fd6b609f1d97f42b4eb7e 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 1e9983dd51eeb43edbba85e04cf4d101be53850b..4da4f942609c8aa048db60978c10cd676ee7c1a6 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 13cd10c72d5b4071f816c4220da8127dab9e61d6..34298d91ee6cd15218eaa30df4b27a7e8ddeae8d 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 60cc76525e90ea1e8fc7d2e36ae6d5fcfa79bca3..27c531dbae2c92e8ed17eb4a5bb62f682ad44956 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 6ee79e67684b87e2579aa0ea4c44deace5f38c2f..fd890b44fd309b9274b16f57b3b612078a9682a2 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 5019c19200ae39b05ed7b5513f0c407adcf5c577..df1151d0372728c581ddaed68ce417a896d07c55 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@ */ /*@