diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i index f74c36d4c224c0f792529bc703b3560a7ac70371..7f41b168b082e3d19f3540484cd7557b03a9c276 100644 --- a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i +++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i @@ -2,7 +2,7 @@ OPT: -wp-gen -wp-rte -wp-prover why3 -wp-msg-key print-generated */ /* run.config_qualif - OPT: -wp-rte -wp-coq-script @PTEST_DIR@/chunk_typing_usable.script -wp-prover alt-ergo,native:coq + OPT: -wp-rte -wp-coq-script %{dep:@PTEST_DIR@/chunk_typing_usable.script} -wp-prover alt-ergo,native:coq */ /*@ diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c index d8defa956ed43e2b5cb2093be2a5b5242f8394fd..8c4932391e6248f70ca55fb5d29ae2b59cb0d332 100644 --- a/src/plugins/wp/tests/wp_acsl/classify_float.c +++ b/src/plugins/wp/tests/wp_acsl/classify_float.c @@ -1,7 +1,7 @@ /* run.config_qualif OPT: -wp-prover alt-ergo OPT: -wp-prover native:alt-ergo - OPT: -wp-prover native:coq -wp-coq-script @PTEST_DIR@/classify_float.script + OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/classify_float.script} OPT: -wp-model real */ diff --git a/src/plugins/wp/tests/wp_acsl/tset.i b/src/plugins/wp/tests/wp_acsl/tset.i index 208066a14375f6af2567fe81ff022c91a0838628..1f7b11df21bbacb99fcbf4de995db036cac04e8d 100644 --- a/src/plugins/wp/tests/wp_acsl/tset.i +++ b/src/plugins/wp/tests/wp_acsl/tset.i @@ -1,5 +1,5 @@ /* run.config_qualif - OPT: -wp -wp-prover alt-ergo,native:coq -wp-coq-script @PTEST_DIR@/tset.s + OPT: -wp -wp-prover alt-ergo,native:coq -wp-coq-script %{dep:@PTEST_DIR@/tset.s} */ /*@ diff --git a/src/plugins/wp/tests/wp_bts/bts_1174.i b/src/plugins/wp/tests/wp_bts/bts_1174.i index f50673b933b25cf3f63ca15ff10fc7c6bef22604..ce50d9189258794e8e0292d0262e3e922e763a83 100644 --- a/src/plugins/wp/tests/wp_bts/bts_1174.i +++ b/src/plugins/wp/tests/wp_bts/bts_1174.i @@ -1,5 +1,5 @@ /* run.config_qualif - OPT: -wp -wp-prover native:coq -wp-coq-script @PTEST_DIR@/bts_1174.s -wp-model +real + OPT: -wp -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/bts_1174.s} -wp-model +real */ /*@ requires -10. <= x && x <= 10.; */ diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c index 708ae7e8df94e667940e4727247cdcaa7fa1b55e..130896edb869eda985da946cc155712452c388bb 100644 --- a/src/plugins/wp/tests/wp_gallery/euclid.c +++ b/src/plugins/wp/tests/wp_gallery/euclid.c @@ -5,7 +5,7 @@ /* run.config_qualif - OPT: -wp-rte -wp-smoke-tests -wp-driver @PTEST_DIR@/euclid.wp + OPT: -wp-rte -wp-smoke-tests -wp-driver %{dep:@PTEST_DIR@/euclid.wp} */ /*@ diff --git a/src/plugins/wp/tests/wp_plugin/region_to_coq.i b/src/plugins/wp/tests/wp_plugin/region_to_coq.i index 1559385fdb5302d5b94264553758701e6e82385e..24ca4a86019fb5939ae553d2d1b18396e78c6a47 100644 --- a/src/plugins/wp/tests/wp_plugin/region_to_coq.i +++ b/src/plugins/wp/tests/wp_plugin/region_to_coq.i @@ -2,7 +2,7 @@ DONTRUN: */ /* run.config_qualif - OPT: -wp-prover native:coq -wp-coq-script @PTEST_DIR@/region_to_coq.script + OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/region_to_coq.script} */ void copy(int* a, unsigned int n, int* b) diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config index c85101d0b58d18ca145d6963a56e1163ad1a7a0e..95a1509ecb2186f18d78ff6184dc767638359d65 100644 --- a/src/plugins/wp/tests/wp_region/test_config +++ b/src/plugins/wp/tests/wp_region/test_config @@ -1,4 +1,4 @@ PLUGIN: wp,rtegen CMD: @frama-c@ LOG: @PTEST_NAME@/region/job.dot -OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job +OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_RESULT@/@PTEST_NAME@ -wp-fct job