From 53967ef50843e5fd1e12200962edcc3ed4d4fbb9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Mar 2022 10:36:45 +0100
Subject: [PATCH] [wp] enable tests in Dune
---
src/plugins/wp/tests/ptests_config | 11 ++---
src/plugins/wp/tests/test_config | 3 +-
src/plugins/wp/tests/test_config_qualif | 3 +-
.../tests/wp_gallery/binary-multiplication.c | 2 +-
src/plugins/wp/tests/wp_gallery/dune | 3 ++
src/plugins/wp/tests/wp_manual/dune | 3 ++
.../wp/tests/wp_plugin/bitmask0x8000.i | 2 +-
src/plugins/wp/tests/wp_plugin/dune | 11 +++++
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/dune | 47 +++++++++++++++++++
src/plugins/wp/tests/wp_tip/induction.i | 6 +--
.../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 +-
.../wp/tests/wp_tip/tac_split_quantifiers.i | 2 +-
src/plugins/wp/tests/wp_tip/unroll.i | 2 +-
19 files changed, 87 insertions(+), 24 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_gallery/dune
create mode 100644 src/plugins/wp/tests/wp_manual/dune
create mode 100644 src/plugins/wp/tests/wp_plugin/dune
create mode 100644 src/plugins/wp/tests/wp_tip/dune
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index ad695944dd3..78e1864b185 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,9 +1,6 @@
# todo: to fixe
-IGNORE= DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-IGNORE= DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
+DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
+DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
-IGNORE= DEFAULT_SUITES= wp_region
-
-IGNORE= qualif_SUITES= wp wp_plugin wp_acsl wp_bts wp_store wp_hoare
-IGNORE= qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip wp_region
-IGNORE= qualif_SUITES= why3
+qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
+qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip why3
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index 1c78f06e11e..9a3cee925ad 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,5 +1,6 @@
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"
+COMMENT: no need of "-wp-share" in Dune -> Dune finds it automatically
+CMD: @frama-c@ -wp -wp-prover none -wp-print -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 895b3f4d8bf..88540550a93 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,5 +1,6 @@
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-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@
+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@
OPT:
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index c365c6f4482..8cf00d59bca 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/*
OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@
*/
diff --git a/src/plugins/wp/tests/wp_gallery/dune b/src/plugins/wp/tests/wp_gallery/dune
new file mode 100644
index 00000000000..4e2c8b817fd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/dune
@@ -0,0 +1,3 @@
+(subdir
+ result_qualif/binary-multiplication.0.session_qualif/script
+ (copy_files ../../../binary-multiplication.0.session_qualif/script/*))
diff --git a/src/plugins/wp/tests/wp_manual/dune b/src/plugins/wp/tests/wp_manual/dune
new file mode 100644
index 00000000000..d97afa29490
--- /dev/null
+++ b/src/plugins/wp/tests/wp_manual/dune
@@ -0,0 +1,3 @@
+(subdir
+ result_qualif/working_dir
+ (copy_files ../../working_dir/*))
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
index e2e5cf5fba3..6dacd120f08 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/*
OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/
diff --git a/src/plugins/wp/tests/wp_plugin/dune b/src/plugins/wp/tests/wp_plugin/dune
new file mode 100644
index 00000000000..7323baff07f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/dune
@@ -0,0 +1,11 @@
+(subdir
+ result_qualif/bitmask0x8000.0.session_qualif/script
+ (copy_files ../../../bitmask0x8000.0.session_qualif/script/*))
+
+(subdir
+ result_qualif/unroll.0.session_qualif/script
+ (copy_files ../../../unroll.0.session_qualif/script/*))
+
+(subdir
+ result_qualif/unsigned.0.session_qualif/script
+ (copy_files ../../../unsigned.0.session_qualif/script/*))
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index 021ceb05d91..ff390357726 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/*
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 a4075988005..3fcc134f879 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/*
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 c4d1b5f5376..b86a92e0c33 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/*
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/dune b/src/plugins/wp/tests/wp_tip/dune
new file mode 100644
index 00000000000..4b359d879b1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/dune
@@ -0,0 +1,47 @@
+; Non qualif
+
+(subdir
+ result/clear.0.session/script
+ (copy_files ../../../clear.0.session/script/*))
+
+(subdir
+ result/induction_typing.0.session/script
+ (copy_files ../../../induction_typing.0.session/script/*))
+
+(subdir
+ result/modmask.0.session/script
+ (copy_files ../../../modmask.0.session/script/*))
+
+(subdir
+ result/modmask.1.session/script
+ (copy_files ../../../modmask.1.session/script/*))
+
+(subdir
+ result/split.0.session/script
+ (copy_files ../../../split.0.session/script/*))
+
+; Qualif
+
+(subdir
+ result_qualif/induction.0.session_qualif/script
+ (copy_files ../../../induction.0.session_qualif/script/*))
+
+(subdir
+ result_qualif/induction.1.session_qualif/script
+ (copy_files ../../../induction.1.session_qualif/script/*))
+
+(subdir
+ result_qualif/induction.2.session_qualif/script
+ (copy_files ../../../induction.2.session_qualif/script/*))
+
+(subdir
+ result_qualif/overflow.0.session_qualif/script
+ (copy_files ../../../overflow.0.session_qualif/script/*))
+
+(subdir
+ result_qualif/tac_split_quantifiers.0.session_qualif/script
+ (copy_files ../../../tac_split_quantifiers.0.session_qualif/script/*))
+
+(subdir
+ result_qualif/unroll.0.session_qualif/script
+ (copy_files ../../../unroll.0.session_qualif/script/*))
diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i
index df4e3fa378d..332d18f3056 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/*
OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
-
+ DEPS: @WP_SESSION@/script/*
OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
-
+ DEPS: @WP_SESSION@/script/*
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 4f9b82169e6..6837f329d7c 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/*
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 4da4f942609..7234784f8de 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/*
OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
-
+ DEPS: @WP_SESSION@/script/*
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 34298d91ee6..66552f291f9 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/*
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 27c531dbae2..0738e2bcd8c 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/*
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 fd890b44fd3..e67c1eca52f 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/*
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 df1151d0372..a8c6e6defc3 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/*
OPT: -wp-prover script,none @USING_WP_SESSION@
*/
--
GitLab