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

[wp] Test for unsupported step limit

parent e72e7812
No related branches found
No related tags found
No related merge requests found
[main]
default_editor = "editor %f"
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5
[prover]
command = "alt-ergo -timelimit %t %f"
driver = "alt_ergo_2_2_0"
in_place = false
interactive = false
name = "no-steps"
/* run.config
DONTRUN:
*/
/* run.config_qualif
CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@
OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-msg-key shell
*/
/*@
lemma truc: \false ;
*/
# frama-c -wp -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/no_step_limit.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] Warning: no-steps does not support steps limit (ignored option)
[wp] [no-steps] Goal typed_lemma_truc : Unsuccess
[wp] Proved goals: 0 / 1
no-steps: 0 (unsuccess: 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