[wp] enable tests in Dune

src/plugins/wp/tests/ptests_config

 # 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

src/plugins/wp/tests/test_config

 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:

src/plugins/wp/tests/test_config_qualif

 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:

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

src/plugins/wp/tests/wp_gallery/dune

+(subdir
+ result_qualif/binary-multiplication.0.session_qualif/script
+ (copy_files ../../../binary-multiplication.0.session_qualif/script/*))

src/plugins/wp/tests/wp_manual/dune

+(subdir
+ result_qualif/working_dir
+ (copy_files ../../working_dir/*))

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

src/plugins/wp/tests/wp_plugin/dune

+(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/*))

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

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

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

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

src/plugins/wp/tests/wp_tip/dune

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

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

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

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

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

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

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

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

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

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

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