From bdfb27ef6a241066d5febe90847c4f58963916db Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 7 Dec 2021 16:13:12 +0100
Subject: [PATCH] [wp tests] adds some more %{dep:file}
---
src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i | 2 +-
src/plugins/wp/tests/wp_acsl/classify_float.c | 2 +-
src/plugins/wp/tests/wp_acsl/tset.i | 2 +-
src/plugins/wp/tests/wp_bts/bts_1174.i | 2 +-
src/plugins/wp/tests/wp_gallery/euclid.c | 2 +-
src/plugins/wp/tests/wp_plugin/region_to_coq.i | 2 +-
src/plugins/wp/tests/wp_region/test_config | 2 +-
7 files changed, 7 insertions(+), 7 deletions(-)
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 f74c36d4c22..7f41b168b08 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 d8defa956ed..8c4932391e6 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 208066a1437..1f7b11df21b 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 f50673b933b..ce50d918925 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 708ae7e8df9..130896edb86 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 1559385fdb5..24ca4a86019 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 c85101d0b58..95a1509ecb2 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
--
GitLab