[wp/region] optimized array test

src/plugins/wp/tests/wp_region/array.c

@@ -18,9 +18,6 @@ void add_first4(struct S * a , struct S * b )
 {
     a->content[0] += b->content[0];
     a->content[1] += b->content[1];
-    note1:
     a->content[2] += b->content[2];
-    //@ assert a!=b ==> a->content[2] == \at(a->content[2],note1) + b->content[2];
-    //@ assert a==b ==> a->content[2] == 2*\at(a->content[2],note1);
     a->content[3] += b->content[3];
 }

src/plugins/wp/tests/wp_region/oracle/array.res.oracle

@@ -4,8 +4,6 @@
 [wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function add_first4
 ------------------------------------------------------------
@@ -14,38 +12,36 @@ Goal Post-condition (file array.c, line 12) in 'add_first4':
 Let a_1 = shiftfield_F1_S_content(a).
 Let a_2 = shift_sint32(a_1, 0).
 Let x = Msint32_0[a_2].
-Let a_3 = shiftfield_F1_S_content(b).
-Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
-Let m = Msint32_0[a_2 <- x + x_1].
-Let a_4 = shift_sint32(a_1, 1).
+Let a_3 = shift_sint32(a_1, 1).
+Let x_1 = Msint32_0[a_3].
+Let a_4 = shift_sint32(a_1, 2).
 Let x_2 = Msint32_0[a_4].
-Let x_3 = m[shift_sint32(a_3, 1)].
-Let m_1 = m[a_4 <- x_2 + x_3].
-Let a_5 = shift_sint32(a_1, 2).
-Let x_4 = Msint32_0[a_5].
-Let a_6 = shift_sint32(a_3, 2).
-Let x_5 = m_1[a_6].
-Let x_6 = x_4 + x_5.
-Let m_2 = m_1[a_5 <- x_6].
-Let a_7 = shift_sint32(a_1, 3).
-Let x_7 = Msint32_0[a_7].
-Let x_8 = m_2[shift_sint32(a_3, 3)].
-Let x_9 = m_2[a_7 <- x_7 + x_8][a_6].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_5 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_5].
+Let x_6 = m_1[a_7].
+Let x_7 = x_2 + x_6.
+Let m_2 = m_1[a_4 <- x_7].
+Let x_8 = m_2[shift_sint32(a_6, 3)].
+Let x_9 = m_2[a_5 <- x_3 + x_8][a_7].
 Assume {
-  Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_4) /\ is_sint32(x_7) /\
-      is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
-      is_sint32(Msint32_0[a_6]) /\ is_sint32(x_3) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_8) /\ is_sint32(x_9).
+  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+      is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+      is_sint32(Msint32_0[a_7]) /\ is_sint32(x_5) /\ is_sint32(x_6) /\
+      is_sint32(x_7) /\ is_sint32(x_8) /\ is_sint32(x_9).
   (* Heap *)
   Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
   (* Goal *)
   When: b != a.
   (* Pre-condition *)
   Have: P_pointed(a, b).
-  (* Assertion *)
-  Have: m_2[a_6] = x_5.
 }
-Prove: x_9 = x_5.
+Prove: x_9 = x_6.
 
 ------------------------------------------------------------
 
@@ -58,77 +54,30 @@ Goal Post-condition (file array.c, line 14) in 'add_first4':
 Let a_1 = shiftfield_F1_S_content(a).
 Let a_2 = shift_sint32(a_1, 0).
 Let x = Msint32_0[a_2].
-Let a_3 = shiftfield_F1_S_content(b).
-Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
-Let m = Msint32_0[a_2 <- x + x_1].
-Let a_4 = shift_sint32(a_1, 1).
-Let x_2 = Msint32_0[a_4].
-Let x_3 = m[shift_sint32(a_3, 1)].
-Let m_1 = m[a_4 <- x_2 + x_3].
-Let a_5 = shift_sint32(a_3, 2).
-Let x_4 = m_1[a_5].
-Let a_6 = shift_sint32(a_1, 2).
-Let x_5 = Msint32_0[a_6].
-Let x_6 = x_5 + x_4.
-Let m_2 = m_1[a_6 <- x_6].
-Let x_7 = m_2[a_5].
-Let a_7 = shift_sint32(a_1, 3).
-Let x_8 = Msint32_0[a_7].
-Let x_9 = Msint32_0[a_5].
-Let x_10 = m_2[shift_sint32(a_3, 3)].
-Assume {
-  Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_8) /\
-      is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
-      is_sint32(x_9) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x_6) /\
-      is_sint32(x_7) /\ is_sint32(x_10) /\
-      is_sint32(m_2[a_7 <- x_8 + x_10][a_5]).
-  (* Heap *)
-  Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
-  (* Pre-condition *)
-  Have: P_pointed(a, b).
-  (* Assertion *)
-  Have: ((b != a) -> (x_7 = x_4)).
-  (* Assertion *)
-  Have: ((b = a) -> (x_4 = x_5)).
-}
-Prove: x_4 = x_9.
-
-------------------------------------------------------------
-
-Goal Post-condition (file array.c, line 15) in 'add_first4':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file array.c, line 23):
-Let a_1 = shiftfield_F1_S_content(a).
-Let a_2 = shift_sint32(a_1, 0).
-Let x = Msint32_0[a_2].
 Let a_3 = shift_sint32(a_1, 1).
 Let x_1 = Msint32_0[a_3].
 Let a_4 = shift_sint32(a_1, 2).
 Let x_2 = Msint32_0[a_4].
-Let a_5 = shiftfield_F1_S_content(b).
-Let x_3 = Msint32_0[shift_sint32(a_5, 0)].
-Let a_6 = shift_sint32(a_5, 2).
-Let m = Msint32_0[a_2 <- x + x_3].
-Let x_4 = m[shift_sint32(a_5, 1)].
-Let m_1 = m[a_3 <- x_1 + x_4].
-Let x_5 = m_1[a_6].
-Let x_6 = x_2 + x_5.
-Let m_2 = m_1[a_4 <- x_6].
-Let x_7 = m_2[a_6].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let x_5 = Msint32_0[a_7].
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_6 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_6].
+Let x_7 = m_1[a_7].
+Let x_8 = x_2 + x_7.
+Let m_2 = m_1[a_4 <- x_8].
+Let x_9 = m_2[shift_sint32(a_6, 3)].
 Assume {
-  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
-      is_sint32(Msint32_0[shift_sint32(a_1, 3)]) /\
-      is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_3) /\
-      is_sint32(Msint32_0[a_6]) /\ is_sint32(x_4) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_7) /\
-      is_sint32(m_2[shift_sint32(a_5, 3)]).
+  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+      is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+      is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(x_8) /\
+      is_sint32(x_9) /\ is_sint32(m_2[a_5 <- x_3 + x_9][a_7]).
   (* Heap *)
   Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
-  (* Goal *)
-  When: b != a.
   (* Pre-condition *)
   Have: P_pointed(a, b).
 }
@@ -136,7 +85,7 @@ Prove: x_7 = x_5.
 
 ------------------------------------------------------------
 
-Goal Assertion (file array.c, line 24):
+Goal Post-condition (file array.c, line 15) in 'add_first4':
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle

@@ -4,21 +4,17 @@
 [wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[wp] 6 goals scheduled
+[wp] 4 goals scheduled
 [wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_add_first4_ensures_2 (Qed)
 [wp] [Valid] region_add_first4_ensures_3 (Alt-Ergo) (Cached)
 [wp] [Valid] region_add_first4_ensures_4 (Qed)
-[wp] [Valid] region_add_first4_assert (Alt-Ergo) (Cached)
-[wp] [Valid] region_add_first4_assert_2 (Qed)
-[wp] Proved goals:    8 / 8
+[wp] Proved goals:    6 / 6
   Terminating:     1
   Unreachable:     1
-  Qed:             3
-  Alt-Ergo:        3
+  Qed:             2
+  Alt-Ergo:        2
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  add_first4                3        3        6       100%
+  add_first4                2        2        4       100%
 ------------------------------------------------------------