From 81fbce4e4496a7de0b15345227d64d4df6d49480 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 23 Mar 2020 16:35:23 +0100
Subject: [PATCH] [wp] test exhibiting the scope problem

---
 src/plugins/wp/tests/wp_bts/issue_837.c       | 15 +++++
 .../tests/wp_bts/oracle/issue_837.res.oracle  | 66 +++++++++++++++++++
 .../wp_bts/oracle_qualif/issue_837.res.oracle | 23 +++++++
 3 files changed, 104 insertions(+)
 create mode 100644 src/plugins/wp/tests/wp_bts/issue_837.c
 create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
 create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle

diff --git a/src/plugins/wp/tests/wp_bts/issue_837.c b/src/plugins/wp/tests/wp_bts/issue_837.c
new file mode 100644
index 00000000000..c266ff99736
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_837.c
@@ -0,0 +1,15 @@
+#define TEST(x) ( x ? 1 : 0 )
+
+//@ assigns \nothing;
+void foo(int a, int b)
+{
+  if (a && TEST(b)) ; else if (TEST(b))
+    {} // BUG: the assigns is not proved by WP 
+}
+
+//@ assigns \nothing;
+void bar(int a, int b)
+{
+  if (a && TEST(b)) ; else if (TEST(b))
+    ; // OK: the assigns is correctly proved by WP
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
new file mode 100644
index 00000000000..2c7f2a6b78d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
@@ -0,0 +1,66 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function bar
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bar' (1/5):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bar' (2/5):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bar' (3/5):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bar' (4/5):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'bar' (5/5):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Assigns nothing in 'foo' (1/4):
+Effect at line 6
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'foo' (2/4):
+Effect at line 6
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'foo' (3/4):
+Effect at line 6
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'foo' (4/4):
+Effect at line 6
+Assume { Type: is_sint32(a). (* Residual *) When: a != 0. }
+Prove: (ta_tmp_0=false).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
new file mode 100644
index 00000000000..a619021a1b9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_837.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 9 goals scheduled
+[wp] [Qed] Goal typed_bar_assigns_part1 : Valid
+[wp] [Qed] Goal typed_bar_assigns_part2 : Valid
+[wp] [Qed] Goal typed_bar_assigns_part3 : Valid
+[wp] [Qed] Goal typed_bar_assigns_part4 : Valid
+[wp] [Qed] Goal typed_bar_assigns_part5 : Valid
+[wp] [Qed] Goal typed_foo_assigns_part1 : Valid
+[wp] [Qed] Goal typed_foo_assigns_part2 : Valid
+[wp] [Qed] Goal typed_foo_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_foo_assigns_part4 : Unsuccess
+[wp] Proved goals:    8 / 9
+  Qed:             8 
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  foo                       3        -        4      75.0%
+  bar                       5        -        5       100%
+------------------------------------------------------------
-- 
GitLab