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 0000000000000000000000000000000000000000..c266ff9973679b4fdf1b44c133f30128062d11e4 --- /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 0000000000000000000000000000000000000000..2c7f2a6b78db6f44db8d357ac2a058fdcd7988fb --- /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 0000000000000000000000000000000000000000..a619021a1b9190554575130a51912421d49b3730 --- /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% +------------------------------------------------------------