[wp tests] adds DEPS directive and %{dep:file}

src/plugins/wp/tests/wp_manual/manual.i

@@ -2,9 +2,9 @@
    DONTRUN:
 */
 /* run.config_qualif
-   OPT: -wp-msg-key shell @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap1.h
-   OPT: -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h
+   OPT: -wp-msg-key shell %{dep:@PTEST_DIR@/working_dir/swap.c} %{dep:@PTEST_DIR@/working_dir/swap1.h}
+   OPT: -wp-msg-key shell -wp-rte %{dep:@PTEST_DIR@/working_dir/swap.c} %{dep:@PTEST_DIR@/working_dir/swap2.h}
 PLUGIN: wp,rtegen,report
-   OPT: -kernel-verbose 0 -wp-msg-key shell -wp-rte @PTEST_DIR@/working_dir/swap.c @PTEST_DIR@/working_dir/swap2.h -wp-verbose 0 -then -no-unicode -report
+   OPT: -kernel-verbose 0 -wp-msg-key shell -wp-rte %{dep:@PTEST_DIR@/working_dir/swap.c} %{dep:@PTEST_DIR@/working_dir/swap2.h} -wp-verbose 0 -then -no-unicode -report
 */
 void look_at_working_dir(void);

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

 /* run.config
-   OPT: -wp-driver tests/wp_plugin/abs.driver
+ COMMENT: depends from files mentionned into "abs.driver"
+ DEPS: abs.why abs.mlw abs.script Abs.v
+   OPT: -wp-driver %{dep:@PTEST_DIR@/abs.driver}
  */
-
 /* run.config_qualif
-   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover alt-ergo
-   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover native:coq -wp-coq-script tests/wp_plugin/abs.script
-   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover native:alt-ergo
+ COMMENT: depends from files mentionned into "abs.driver"
+ DEPS: abs.why abs.mlw abs.script Abs.v
+   OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover alt-ergo
+   OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/abs.script}
+   OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover native:alt-ergo
 */
-
 /*@ axiomatic Absolute { logic integer ABS(integer x) ; } */
 
 /*@ ensures \result == ABS(x) ; */

src/plugins/wp/tests/wp_plugin/bit_test.c

 /* run.config
-   OPT: -wp-driver tests/wp_plugin/bit_test.driver
+   OPT: -wp-driver %{dep:@PTEST_DIR@/bit_test.driver}
  */
 
 /* run.config_qualif
-   OPT: -wp-driver tests/wp_plugin/bit_test.driver -wp-prover why3:alt-ergo
+   OPT: -wp-driver %{dep:@PTEST_DIR@/bit_test.driver} -wp-prover why3:alt-ergo
 */
 
 /*@

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

@@ -3,6 +3,6 @@
 */
 
 /* run.config_qualif
-   CMD: tests/wp_plugin/config.sh
+   CMD: %{dep:@PTEST_DIR@/config.sh}
    OPT:
 */

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

@@ -4,7 +4,7 @@
 
 /* run.config_qualif
    OPT:
-   OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report
+   OPT: -wp-prover native:alt-ergo -wp-report=%{dep:tests/native.report}
 */
 
 // --------------------------------------------------------------------------

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

@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-smoke-tests -wp-report tests/wp_plugin/doomed.report
+   OPT: -wp-smoke-tests -wp-report %{dep:@PTEST_DIR@/doomed.report}
 */
 
 /*@ axiomatic CFG {

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

@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-smoke-tests -wp-report tests/wp_plugin/doomed.report
+   OPT: -wp-smoke-tests -wp-report %{dep:@PTEST_DIR@/doomed.report}
 */
 
 /*@ axiomatic CFG {

src/plugins/wp/tests/wp_plugin/flash.c

 /* run.config
    OPT:
-   OPT: -wp-driver tests/wp_plugin/flash.driver,tests/wp_plugin/flash-ergo.driver
+ DEPS: flash.mlw
+   OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver},%{dep:@PTEST_DIR@/flash-ergo.driver}
 SCRIPT: flash
-   OPT: -wp-driver tests/wp_plugin/flash.driver
+   OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver}
 */
+
 /* run.config_qualif
    OPT: -wp-timeout 1
-   OPT: -wp-driver tests/wp_plugin/flash.driver,tests/wp_plugin/flash-ergo.driver
-SCRIPT: flash
-   OPT: -wp-driver tests/wp_plugin/flash.driver
+ DEPS: flash.mlw
+   OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver},%{dep:@PTEST_DIR@/flash-ergo.driver}
+SCRIPT: @PTEST_NAME@
+   OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver}
 */
+
 /* -------------------------------------------------------------------------- */
 /* --- Observation of Sequence of Reads and Writes                        --- */
 /* -------------------------------------------------------------------------- */

src/plugins/wp/tests/wp_plugin/inductive.c

@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover native:coq -wp-coq-script tests/wp_plugin/inductive.script -wp-timeout 240
+   OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/inductive.script} -wp-timeout 240
 */
 
 typedef struct _list { int element; struct _list* next; } list;

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

 /* run.config
-   OPT: tests/wp_plugin/init_linker.i
+   OPT: %{dep:@PTEST_DIR@/init_linker.i}
  */
 
 /* run.config_qualif
-   OPT: tests/wp_plugin/init_linker.i
+   OPT: %{dep:@PTEST_DIR@/init_linker.i}
  */
 
 // To be linked with init_linker that defines the initial value of 'a'

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

@@ -3,10 +3,10 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover alt-ergo                                            -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
-   OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report      -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
-   OPT: -wp-prover alt-ergo                                            -wp-prop=ko   -wp-timeout 100 -wp-steps 10
-   OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report      -wp-prop=ko   -wp-timeout 100 -wp-steps 10
+   OPT: -wp-prover alt-ergo                                              -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
+   OPT: -wp-prover native:alt-ergo -wp-report=%{dep:tests/native.report} -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
+   OPT: -wp-prover alt-ergo                                              -wp-prop=ko   -wp-timeout 100 -wp-steps 10
+   OPT: -wp-prover native:alt-ergo -wp-report=%{dep:tests/native.report} -wp-prop=ko   -wp-timeout 100 -wp-steps 10
 */
 
 // --------------------------------------------------------------------------

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

@@ -2,10 +2,13 @@
   DONTRUN:
 */
 /* run.config_qualif
+ 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
 */
+
 // cache is locally deactivated to see the option
+
 /*@
   lemma truc: \false ;
 */

src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle

@@ -6,7 +6,7 @@
   Function abs
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/abs.i, line 13) in 'abs':
+Goal Post-condition (file tests/wp_plugin/abs.i, line 15) in 'abs':
 Assume {
   Type: is_sint32(abs_0) /\ is_sint32(x).
   If x < 0

src/plugins/wp/tests/wp_region/annot.i

 /* run.config
    PLUGIN: wp
    OPT: -region-annot -print
-   EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ @PTEST_DIR@/@PTEST_NAME@.i            -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
-   EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
-   EXECNOW: LOG  diff_@PTEST_NAME@.txt diff @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
+   EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ %{dep:@PTEST_DIR@/@PTEST_NAME@.i}            -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
+   EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
+   EXECNOW: LOG  diff_@PTEST_NAME@.txt diff %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_2.i} &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
 COMMENT: The file diff_@PTEST_NAME@.txt must be empty.
 COMMENT: So, that file has not to be present into the oracle directory since absent files are considered such as empty files.
  */

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

 /* run.config
+ DEPS: unit_bitwise.h
    OPT:
 */
 /* run.config_qualif
+ DEPS: unit_bitwise.h
    OPT: -wp-prop="-ko"
    OPT: -wp-prop="ko"
 */
 
-
-
 #include "unit_bitwise.h"
 //===============================================
 //-- int

src/plugins/wp/tests/wp_usage/save_load.i

 /* run.config
-   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
-   CMD: @frama-c@ -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
+   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@.sav.res 2> @PTEST_RESULT@/@PTEST_NAME@.sav.err
+   CMD: @frama-c@ -load %{dep:@PTEST_RESULT@/@PTEST_NAME@.sav} -wp-warn-key pedantic-assigns=inactive
    OPT: -print
    OPT: -wp -wp-prover none -wp-print
 */