From ac162941ae03a4b21ed89a2542e5de73a14c40a5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 9 Sep 2020 15:35:29 +0200
Subject: [PATCH] [wp] Test for unsupported step limit

---
 src/plugins/wp/tests/wp_plugin/no_step_limit.conf   | 13 +++++++++++++
 src/plugins/wp/tests/wp_plugin/no_step_limit.i      | 10 ++++++++++
 .../oracle_qualif/no_step_limit.res.oracle          |  8 ++++++++
 3 files changed, 31 insertions(+)
 create mode 100644 src/plugins/wp/tests/wp_plugin/no_step_limit.conf
 create mode 100644 src/plugins/wp/tests/wp_plugin/no_step_limit.i
 create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle

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 00000000000..8431029cc72
--- /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 00000000000..2d5745aa584
--- /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 00000000000..0aeeeccf367
--- /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)
-- 
GitLab