[wp] More tests on base_offset

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) ;
+}

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

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