From 07110e9b35406e0ef4080e6158c6947215d579de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 13 May 2020 08:40:18 +0200
Subject: [PATCH] [wp] introduce test case to show bug
---
src/plugins/wp/tests/wp/cfg_loop.i | 55 ++++++++
.../wp/tests/wp/oracle/cfg_loop.res.oracle | 126 ++++++++++++++++++
.../wp/oracle_qualif/cfg_loop.res.oracle | 30 +++++
3 files changed, 211 insertions(+)
create mode 100644 src/plugins/wp/tests/wp/cfg_loop.i
create mode 100644 src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
diff --git a/src/plugins/wp/tests/wp/cfg_loop.i b/src/plugins/wp/tests/wp/cfg_loop.i
new file mode 100644
index 00000000000..7b92f762459
--- /dev/null
+++ b/src/plugins/wp/tests/wp/cfg_loop.i
@@ -0,0 +1,55 @@
+/* -------------------------------------------------------------------------- */
+/* --- Bugs related to CFG for loops & switch --- */
+/* -------------------------------------------------------------------------- */
+
+// All contract shall be provable
+
+void loop_switch(int *a,int c)
+{
+ *a = 1;
+ int b = 2;
+ /*@
+ loop invariant b == 2;
+ loop invariant *a ==1;
+ loop assigns b, *a;
+ */
+ while(1) {
+ switch (c) {
+ case 1:
+ *a = 1;
+ b = 2;
+ break;
+ case 2:
+ b = 2;
+ *a = 1;
+ break;
+ default:
+ *a =1;
+ b = 2;
+ break;
+ }
+ }
+}
+
+int a;
+
+void loop_continue(int x,int y)
+{
+ int *p = &a;
+ /*@
+ loop invariant p == \at(p, LoopEntry);
+ loop assigns *p, x;
+ */
+ while(1)
+ {
+ if(x)
+ {
+ if (y)
+ continue;
+ *p = 1;
+ x++;
+ }
+ else
+ return;
+ }
+}
diff --git a/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
new file mode 100644
index 00000000000..02656daf1c4
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/cfg_loop.res.oracle
@@ -0,0 +1,126 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function loop_continue
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 40):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp/cfg_loop.i, line 40):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 41) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 41) (2/2):
+Effect at line 43
+Let a = global(G_a_28).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, 1).
+ (* Then *)
+ Have: x != 0.
+}
+Prove: a = p.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function loop_switch
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 12) (1/3):
+Tags: Default.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 12) (2/3):
+Tags: Case 2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 12) (3/3):
+Tags: Case 1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp/cfg_loop.i, line 12):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 13) (1/3):
+Tags: Default.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 13) (2/3):
+Tags: Case 2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp/cfg_loop.i, line 13) (3/3):
+Tags: Case 1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp/cfg_loop.i, line 13):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 14) (1/4):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 14) (2/4):
+Effect at line 16
+Tags: Default.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 14) (3/4):
+Effect at line 16
+Tags: Case 2.
+Assume {
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, 1).
+}
+Prove: a = a_1.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop.i, line 14) (4/4):
+Effect at line 16
+Tags: Case 1.
+Assume {
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, 1).
+}
+Prove: a = a_1.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
new file mode 100644
index 00000000000..22585f0cbc1
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
@@ -0,0 +1,30 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 16 goals scheduled
+[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_loop_continue_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_loop_continue_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_loop_continue_loop_assigns_part2 : Unsuccess
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part1 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part2 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part3 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part1 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part2 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_preserved_part3 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_invariant_2_established : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_loop_switch_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_loop_switch_loop_assigns_part3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_switch_loop_assigns_part4 : Unsuccess
+[wp] Proved goals: 13 / 16
+ Qed: 13
+ Alt-Ergo: 0 (unsuccess: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ loop_switch 10 - 12 83.3%
+ loop_continue 3 - 4 75.0%
+------------------------------------------------------------
--
GitLab