[wp] test exhibiting the scope problem

src/plugins/wp/tests/wp_bts/issue_837.c

+#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
+}

src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle

+# 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%
+------------------------------------------------------------