From 750e38f2d40d5e89223459f552403ac2e748d1e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 19 Feb 2020 10:23:45 +0100
Subject: [PATCH] [wp] added test for loop-current

---
 src/plugins/wp/tests/wp_bts/issue_801.i       | 18 +++++++++
 .../tests/wp_bts/oracle/issue_801.res.oracle  | 39 +++++++++++++++++++
 .../c45214be00ee9772cbc817e818d45cff.json     |  2 +
 .../wp_bts/oracle_qualif/issue_801.res.oracle | 19 +++++++++
 4 files changed, 78 insertions(+)
 create mode 100644 src/plugins/wp/tests/wp_bts/issue_801.i
 create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
 create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json
 create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle

diff --git a/src/plugins/wp/tests/wp_bts/issue_801.i b/src/plugins/wp/tests/wp_bts/issue_801.i
new file mode 100644
index 00000000000..8325393b05d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_801.i
@@ -0,0 +1,18 @@
+int a ;
+
+/*@
+  requires a == 1;
+  ensures a == 1;
+*/
+void LoopCurrent()
+{
+  /*@
+    loop assigns s,a;
+    loop invariant A: \at(a, LoopCurrent)== 1;
+    loop variant 10-s;
+  */
+  for(int s = 0; s< 10; s++)
+    {
+      a = 2;
+    }
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
new file mode 100644
index 00000000000..23bbba6733f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
@@ -0,0 +1,39 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function LoopCurrent
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_801.i, line 5) in 'LoopCurrent':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'A' (file tests/wp_bts/issue_801.i, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'A' (file tests/wp_bts/issue_801.i, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_801.i, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_bts/issue_801.i, line 14):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_bts/issue_801.i, line 14):
+Assume { Type: is_sint32(s). (* Then *) Have: s <= 9. }
+Prove: s <= 10.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json
new file mode 100644
index 00000000000..08344e3edd6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0078,
+  "steps": 8 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
new file mode 100644
index 00000000000..5da74e21776
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_801.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_LoopCurrent_ensures : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_preserved : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_established : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_assigns : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_LoopCurrent_loop_variant_positive : Valid
+[wp] Proved goals:    6 / 6
+  Qed:               5 
+  Alt-Ergo 2.0.0:    1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  LoopCurrent               5        1        6       100%
+------------------------------------------------------------
-- 
GitLab