[WP] tests - Adds explicit deps to WP cache env_var

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:

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

src/plugins/wp/tests/wp_plugin/abs.i

 /* 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) ; } */

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/plugins/wp/tests/wp_typed/unit_bitwise.c

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