Skip to content
Snippets Groups Projects
Commit bdfb27ef authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp tests] adds some more %{dep:file}

parent 9e8274e1
No related branches found
No related tags found
No related merge requests found
......@@ -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
*/
/*@
......
/* 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
*/
......
/* 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}
*/
/*@
......
/* 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.; */
......
......@@ -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}
*/
/*@
......
......@@ -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)
......
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment