From a18e6600d153e9525de15f88067f3b39c021227c Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 4 Jul 2022 14:38:07 +0200
Subject: [PATCH] [WP] tests - Adds explicit deps to WP cache env_var
---
src/plugins/wp/tests/test_config_qualif | 3 ++-
src/plugins/wp/tests/wp_gallery/binary-multiplication.c | 2 +-
src/plugins/wp/tests/wp_plugin/abs.i | 4 ++--
src/plugins/wp/tests/wp_plugin/bitmask0x8000.i | 2 +-
src/plugins/wp/tests/wp_plugin/no_step_limit.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 +-
src/plugins/wp/tests/wp_typed/unit_bitwise.c | 4 ++--
16 files changed, 22 insertions(+), 21 deletions(-)
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 88540550a93..e32bb2e32fc 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 2db759273d8..26c0459f04a 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 a602a11d813..441f0356840 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 b00b4902060..889dd60a91d 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 9f3b47813e5..874baf0c74f 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 d42bda0c3d5..f6feda1b587 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 bdc84346f2a..b810f6a8c35 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 cc1ba10ac8a..7f256f87384 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 3e74960fa48..fc876e51ec8 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 2a2771df273..499aff1fb17 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 9437a5a3e85..5d922c9cd7e 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 d9d14829442..9eaeb2f5965 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 f7d03a503c3..5755a39ee51 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 994571f3059..1b30e034e1f 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 7b09c6963fc..f7d00c3009a 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 acb4398b437..76102d7b33f 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"
*/
--
GitLab