diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif index 88540550a9366129e95838e54ecec40e5315583b..e32bb2e32fceb91f4d09937bd09ef630b243ae32 100644 --- a/src/plugins/wp/tests/test_config_qualif +++ b/src/plugins/wp/tests/test_config_qualif @@ -2,5 +2,6 @@ PLUGIN: wp MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ MACRO: USING_WP_SESSION -wp-session @WP_SESSION@ COMMENT: no need of "-wp-share" in Dune -> Dune finds it automatically -CMD: @frama-c@ -wp -wp-par 1 -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@ +CMD: @frama-c@ -wp -wp-par 1 -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env @PTEST_FILE@ +DEPS: env_var:FRAMAC_WP_CACHE env_var:FRAMAC_WP_CACHEDIR OPT: diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c index 2db759273d8a209ac6ea96bafc3522c42a9598e8..26c0459f04acd1eb51b56e24764c26360ba62f6d 100644 --- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c +++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/BinaryMultiplication_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/BinaryMultiplication_*.json OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_plugin/abs.i b/src/plugins/wp/tests/wp_plugin/abs.i index a602a11d813578ba99b10380fa702855e49c3e30..441f0356840d6ed89db4f26bd23b02bd2fa1a393 100644 --- a/src/plugins/wp/tests/wp_plugin/abs.i +++ b/src/plugins/wp/tests/wp_plugin/abs.i @@ -1,11 +1,11 @@ /* run.config COMMENT: depends from files mentionned into "abs.driver" - DEPS: abs.why + DEPS: @PTEST_DEPS@ abs.why OPT: -wp-driver %{dep:@PTEST_DIR@/abs.driver} */ /* run.config_qualif COMMENT: depends from files mentionned into "abs.driver" - DEPS: abs.why + DEPS: @PTEST_DEPS@ abs.why OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover alt-ergo */ /*@ axiomatic Absolute { logic integer ABS(integer x) ; } */ diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i index b00b49020602e59a42e532d69d609ffd12549dfd..889dd60a91da9e01ea85bbfde51f9258537c3940 100644 --- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i +++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_plugin/no_step_limit.i b/src/plugins/wp/tests/wp_plugin/no_step_limit.i index 9f3b47813e5d5248effb9906fee3e8af9131caa5..874baf0c74f20fa9a2510a1cbc783138caedaf2a 100644 --- a/src/plugins/wp/tests/wp_plugin/no_step_limit.i +++ b/src/plugins/wp/tests/wp_plugin/no_step_limit.i @@ -2,7 +2,7 @@ DONTRUN: */ /* run.config_qualif - DEPS: @PTEST_NAME@.conf + DEPS: @PTEST_DEPS@ @PTEST_NAME@.conf CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@ OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-timeout 1 -wp-cache none -wp-no-cache-env -wp-msg-key shell */ diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i index d42bda0c3d540694900bdde8c5017002b0eac26e..f6feda1b587b987794cc4103c1e4e3ea853c7af4 100644 --- a/src/plugins/wp/tests/wp_plugin/unroll.i +++ b/src/plugins/wp/tests/wp_plugin/unroll.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/unrolled_loop_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/unrolled_loop_*.json OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i index bdc84346f2afb07c499bbaf9706efb018fe2b163..b810f6a8c35fc77831675da1bd3c84e5b8ff00a4 100644 --- a/src/plugins/wp/tests/wp_plugin/unsigned.i +++ b/src/plugins/wp/tests/wp_plugin/unsigned.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json 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 cc1ba10ac8a54f6dfe5e85b611bda12bb0c194f0..7f256f8738439fc95f4d5c2bcbb84b230aaa9ec8 100644 --- a/src/plugins/wp/tests/wp_tip/clear.i +++ b/src/plugins/wp/tests/wp_tip/clear.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/clear_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/clear_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i index 3e74960fa48709f83fefc88479d3681a106b3a92..fc876e51ec8686bda8930290c1c0dd625bfe01a9 100644 --- a/src/plugins/wp/tests/wp_tip/induction.i +++ b/src/plugins/wp/tests/wp_tip/induction.i @@ -3,11 +3,11 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/induction_typing.i b/src/plugins/wp/tests/wp_tip/induction_typing.i index 2a2771df273fb410150907a3c5168e0e0db9d9f7..499aff1fb178c673b154735709a9de8af5903dd7 100644 --- a/src/plugins/wp/tests/wp_tip/induction_typing.i +++ b/src/plugins/wp/tests/wp_tip/induction_typing.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/function_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/function_*.json OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i index 9437a5a3e8529f3d4fb5eaee89e6c7349a16a3a1..5d922c9cd7e61fba2d743760a8a2fcd6ada25717 100644 --- a/src/plugins/wp/tests/wp_tip/modmask.i +++ b/src/plugins/wp/tests/wp_tip/modmask.i @@ -1,7 +1,7 @@ /* run.config - DEPS: @WP_SESSION@/script/check_lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/check_lemma_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/check_lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/check_lemma_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/overflow.i b/src/plugins/wp/tests/wp_tip/overflow.i index d9d14829442cbd3c0ee6ae9a54f77df7059914e4..9eaeb2f596507759f4d3d1dbb8736bf679b15ff8 100644 --- a/src/plugins/wp/tests/wp_tip/overflow.i +++ b/src/plugins/wp/tests/wp_tip/overflow.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i index f7d03a503c3723bf03e74775aa2eeaefd214ac94..5755a39ee518534b768f43f4ee77b27c706eb6b3 100644 --- a/src/plugins/wp/tests/wp_tip/split.i +++ b/src/plugins/wp/tests/wp_tip/split.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/test_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/test_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif 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 994571f3059ca385cc52505ce4f8c61aaae7bdc2..1b30e034e1faaac5ab59dd13a59fd4eb1a66cfce 100644 --- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i +++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i @@ -4,7 +4,7 @@ /* run.config_qualif SCRIPT: TacNOP - DEPS: @WP_SESSION@/script/split_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/split_*.json 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 7b09c6963fcd67163de0cf8fd37c18b60bf84b3e..f7d00c3009ab837ca628afb63abb2805118e5126 100644 --- a/src/plugins/wp/tests/wp_tip/unroll.i +++ b/src/plugins/wp/tests/wp_tip/unroll.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/lemma_*.json + DEPS: @PTEST_DEPS@ @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,none @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_typed/unit_bitwise.c b/src/plugins/wp/tests/wp_typed/unit_bitwise.c index acb4398b437fd953eeae6b3d8f23e91a3557fcfb..76102d7b33ff4937ee298883f8648ca44dbc0ec7 100644 --- a/src/plugins/wp/tests/wp_typed/unit_bitwise.c +++ b/src/plugins/wp/tests/wp_typed/unit_bitwise.c @@ -1,9 +1,9 @@ /* run.config - DEPS: unit_bitwise.h + DEPS: @PTEST_DEPS@ unit_bitwise.h OPT: */ /* run.config_qualif - DEPS: unit_bitwise.h + DEPS: @PTEST_DEPS@ unit_bitwise.h OPT: -wp-prop="-ko" OPT: -wp-prop="ko" */