From e70554a715b9b612a408ece17b32fe8afcc9dcbc Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 1 Jul 2022 14:50:47 +0200
Subject: [PATCH] [WP] tests: modifies DEPS using a joker
---
src/plugins/wp/tests/wp_plugin/bitmask0x8000.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 +-
11 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
index 6dacd120f08..b00b4902060 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/*
+ DEPS: @WP_SESSION@/script/lemma_*.json
OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index ff390357726..d42bda0c3d5 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/*
+ 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 3fcc134f879..bdc84346f2a 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/*
+ 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 b86a92e0c33..cc1ba10ac8a 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/*
+ 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 332d18f3056..3e74960fa48 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/*
+ DEPS: @WP_SESSION@/script/lemma_*.json
OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
- DEPS: @WP_SESSION@/script/*
+ DEPS: @WP_SESSION@/script/lemma_*.json
OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
- DEPS: @WP_SESSION@/script/*
+ 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 6837f329d7c..2a2771df273 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/*
+ 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 7234784f8de..9437a5a3e85 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/*
+ 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/*
+ 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 66552f291f9..d9d14829442 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/*
+ 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 0738e2bcd8c..f7d03a503c3 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/*
+ 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 e67c1eca52f..994571f3059 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/*
+ 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 a8c6e6defc3..7b09c6963fc 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/*
+ DEPS: @WP_SESSION@/script/lemma_*.json
OPT: -wp-prover script,none @USING_WP_SESSION@
*/
--
GitLab