Skip to content
Snippets Groups Projects
Commit 379952f9 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Move session directories

- insert place holders for Dune tests
parent 41c9eec7
No related branches found
No related tags found
No related merge requests found
Showing
with 12 additions and 4 deletions
PLUGIN: wp
CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report @PTEST_SUITE_DIR@/../qualif.report -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@
CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report @PTEST_SUITE_DIR@/../qualif.report -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@ -wp-cache-env -wp-cache replay @PTEST_FILE@
OPT:
......@@ -3,6 +3,7 @@
*/
/* run.config_qualif
OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack
*/
......
......@@ -3,6 +3,7 @@
*/
/* run.config_qualif
OPT: -wp-prover script,alt-ergo
*/
......
......@@ -2,7 +2,7 @@
[kernel] Parsing unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] unroll.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Function unrolled_loop
------------------------------------------------------------
......
......@@ -2,7 +2,7 @@
[kernel] Parsing unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] unroll.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Script] Goal typed_unrolled_loop_ensures_zero : Valid
[wp] Proved goals: 1 / 1
......
......@@ -3,6 +3,7 @@
*/
/* run.config_qualif
OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script
*/
......
......@@ -3,6 +3,7 @@
*/
/* run.config_qualif
OPT: -wp-prover script
*/
......
/* run.config
OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session
*/
/* run.config_qualif
DONTRUN:
......
......@@ -3,8 +3,11 @@
*/
/* run.config_qualif
OPT: -wp-prover script,alt-ergo -wp-timeout 1
OPT: -wp-prover script,alt-ergo -wp-timeout 1
OPT: -wp-prover script,alt-ergo -wp-timeout 1
*/
......
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