diff --git a/src/plugins/wp/tests/wp_acsl/base_offset.i b/src/plugins/wp/tests/wp_acsl/base_offset.i index e4e96b65f5cdde8755869bef121630d0f3d89fc6..f38f29df60fc2fa730ca2a467efc810b7f90ba49 100644 --- a/src/plugins/wp/tests/wp_acsl/base_offset.i +++ b/src/plugins/wp/tests/wp_acsl/base_offset.i @@ -16,3 +16,16 @@ struct S* p ; \offset( &p->a[i] ) <= \offset( &p->a[j] ) ; */ void f(void){return;} + +struct { int a ; int b ; } x ; +struct { int a ; int b ; } y ; +struct { double a ; int b ; } z ; + +void g(void){ + int *xb = &x.b; + int *yb = &y.b; + int *zb = &z.b; + + //@ check KO: \offset(xb) == \offset(zb) ; + //@ check KO: \offset(xb) != \offset(yb) ; +} diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle index fcc2455baeae82ac1722ad99c3f67407b3584eb2..3876073ea1f0779069ebc1b7112d194e2da6d937 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle @@ -29,3 +29,16 @@ Assume { Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2). ------------------------------------------------------------ +------------------------------------------------------------ + Function g +------------------------------------------------------------ + +Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 29): +Prove: base_offset_table(G_z_33) = base_offset_table(G_x_31). + +------------------------------------------------------------ + +Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 30): +Prove: base_offset_table(G_y_32) != base_offset_table(G_x_31). + +------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle index 8b29211f4ecea61d71ded5c45410d36fc265b4fb..05b7c9c11f25194d55795c9aba8475fecd23d1f0 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle @@ -2,14 +2,17 @@ [kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 3 goals scheduled +[wp] 5 goals scheduled [wp] [Qed] Goal typed_f_ensures : Valid [wp] [Qed] Goal typed_f_ensures_2 : Valid [wp] [Alt-Ergo] Goal typed_f_ensures_3 : Valid -[wp] Proved goals: 3 / 3 +[wp] [Alt-Ergo] Goal typed_g_check_KO : Unsuccess +[wp] [Alt-Ergo] Goal typed_g_check_KO_2 : Unsuccess +[wp] Proved goals: 3 / 5 Qed: 2 - Alt-Ergo: 1 + Alt-Ergo: 1 (unsuccess: 2) ------------------------------------------------------------ Functions WP Alt-Ergo Total Success f 2 1 3 100% + g - - 2 0.0% ------------------------------------------------------------