From 41a62d0033f139094f64d784a1805ef275b13e19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 16 Mar 2020 19:11:42 +0100
Subject: [PATCH] [wp] added test for integer quantifiers
---
src/plugins/wp/tests/wp_bts/issue_825.i | 16 ++++++++
.../tests/wp_bts/oracle/issue_825.res.oracle | 40 +++++++++++++++++++
.../wp_bts/oracle_qualif/issue_825.res.oracle | 18 +++++++++
3 files changed, 74 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_bts/issue_825.i
create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
diff --git a/src/plugins/wp/tests/wp_bts/issue_825.i b/src/plugins/wp/tests/wp_bts/issue_825.i
new file mode 100644
index 00000000000..b4c514fccc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_825.i
@@ -0,0 +1,16 @@
+/*@
+ ensures \false ;
+ assigns \nothing;
+*/
+void job(void)
+{
+ int i=0, K=0;
+ /*@
+ loop invariant \forall integer j; 0 < j < 0 ==> \false ;
+ loop assigns i ;
+ */
+ while (i < 10) {
+ K ++;
+ i ++;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
new file mode 100644
index 00000000000..8bbd713c28c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
@@ -0,0 +1,40 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_825.i, line 2) in 'job':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
new file mode 100644
index 00000000000..09e0f30d5ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Qed] Goal typed_job_ensures : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals: 6 / 6
+ Qed: 6
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 6 - 6 100%
+------------------------------------------------------------
--
GitLab