diff --git a/src/plugins/wp/tests/wp_plugin/no_step_limit.conf b/src/plugins/wp/tests/wp_plugin/no_step_limit.conf new file mode 100644 index 0000000000000000000000000000000000000000..8431029cc72c4dc267bef9b413c03d74406ae297 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/no_step_limit.conf @@ -0,0 +1,13 @@ +[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" diff --git a/src/plugins/wp/tests/wp_plugin/no_step_limit.i b/src/plugins/wp/tests/wp_plugin/no_step_limit.i new file mode 100644 index 0000000000000000000000000000000000000000..2d5745aa584f56360e7e8ae129266313c25b514c --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/no_step_limit.i @@ -0,0 +1,10 @@ +/* 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 ; +*/ diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..0aeeeccf367612ea83cffeda8d96603923e5c18f --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle @@ -0,0 +1,8 @@ +# 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)