diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 7b2ee670197d932dff8496a82ff39a1942ec57ef..3981469580e3d4711777c2012a00f3807db07930 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -2,14 +2,18 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
+[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 3) in 'init':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 10) in 'init':
Let a_1 = shift_sint32(a, 0).
Assume {
Type: is_sint32(i) /\ is_sint32(n).
@@ -31,7 +35,7 @@ Prove: havoc(Mint_undef_0, Mint_0, a_1, i)[shift_sint32(a, i_1)] = v.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 9):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 17):
Let a_1 = shift_sint32(a, 0).
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
Assume {
@@ -54,12 +58,12 @@ Prove: a_2[shift_sint32(a, i) <- v][shift_sint32(a, i_1)] = v.
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 9):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 17):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 8):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 16):
Let a_1 = shift_sint32(a, 0).
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
@@ -79,18 +83,18 @@ Prove: (-1) <= i.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 8):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 16):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 10) (1/2):
+Goal Loop assigns 'Zone' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 10) (2/2):
-Effect at line 12
+Goal Loop assigns 'Zone' (2/2):
+Effect at line 20
Let a_1 = shift_sint32(a, 0).
Let a_2 = shift_sint32(a, i).
Assume {
@@ -113,8 +117,18 @@ Prove: included(a_2, 1, a_1, n).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 4) in 'init':
-Effect at line 12
+Goal Assigns (file tests/wp_typed/user_init.i, line 9) in 'init':
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 20):
Prove: true.
------------------------------------------------------------
@@ -122,7 +136,7 @@ Prove: true.
Function init_t1
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 16) in 'init_t1':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 24) in 'init_t1':
Assume {
Type: is_uint32(i_1).
(* Goal *)
@@ -134,78 +148,1150 @@ Assume {
(* Else *)
Have: 10 <= i_1.
}
-Prove: t1_0[i] = v.
+Prove: t1_0[i] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 32):
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: t1_0[i <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 31):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 31):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'Zone':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 26) in 'init_t1' (1/2):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 26) in 'init_t1' (2/2):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 35):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 35):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis_v1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 125) in 'init_t2_bis_v1':
+Let a = global(G_t2_48).
+Assume {
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_1 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_1)))))) ->
+ (Mint_1[a_1] = Mint_0[a_1])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i_2) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Else *)
+ Have: 10 <= i_2.
+}
+Prove: Mint_0[shift_sint32(shift_A20_sint32(a, i), i_1)] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_4 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_4)))))) ->
+ (Mint_1[a_4] = Mint_0[a_4])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (a_3[shift_sint32(a_1, i_3)] = v))).
+}
+Prove: a_3[shift_sint32(shift_A20_sint32(a, i_1), i_2)] = Mint_undef_0[a_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 139):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (2/3):
+Effect at line 137
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_3)] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (3/3):
+Call Effect at line 138
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_3), i_2) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_3), i_2)] = v))))).
+ (* Invariant 'Range' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_2)] = v))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (1/3):
+Effect at line 137
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (2/3):
+Effect at line 137
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (3/3):
+Call Effect at line 138
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (1/2):
+Effect at line 137
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (2/2):
+Effect at line 137
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 7) in 'init'' in 'init_t2_bis_v1' at call 'init' (file tests/wp_typed/user_init.i, line 138)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 8) in 'init'' in 'init_t2_bis_v1' at call 'init' (file tests/wp_typed/user_init.i, line 138)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis_v2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 143) in 'init_t2_bis_v2':
+Let a = global(G_t2_48).
+Assume {
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_1 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_1)))) ->
+ (Mint_1[a_1] = Mint_0[a_1])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i_2) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Else *)
+ Have: 10 <= i_2.
+}
+Prove: Mint_0[shift_sint32(shift_A20_sint32(a, i), i_1)] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 145) in 'init_t2_bis_v2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_4 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_4)))) ->
+ (Mint_1[a_4] = Mint_0[a_4])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (a_3[shift_sint32(a_1, i_3)] = v))).
+}
+Prove: a_3[shift_sint32(shift_A20_sint32(a, i_1), i_2)] = Mint_undef_0[a_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 157):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (2/3):
+Effect at line 155
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i_2).
+Assume {
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_6), i_5) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_6), i_5)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Then *)
+ Have: i_2 <= 9.
+ (* Call 'init' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_5)] = v))).
+}
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (3/3):
+Call Effect at line 156
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_3), i_2) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_3), i_2)] = v))))).
+ (* Invariant 'Range' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_2)] = v))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
+ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (1/3):
+Effect at line 155
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (2/3):
+Effect at line 155
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (3/3):
+Call Effect at line 156
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (1/2):
+Effect at line 155
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (2/2):
+Effect at line 155
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 7) in 'init'' in 'init_t2_bis_v2' at call 'init' (file tests/wp_typed/user_init.i, line 156)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 8) in 'init'' in 'init_t2_bis_v2' at call 'init' (file tests/wp_typed/user_init.i, line 156)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_v1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 39) in 'init_t2_v1':
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 48):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 48):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 47):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 47):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 54):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: m[j <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 54):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 55):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (m[i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 55):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 53):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 53):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 64):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_i' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_i' (2/3):
+Effect at line 51
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Goal Loop assigns 'lack,Zone_i' (3/3):
+Effect at line 58
Assume {
Type: is_uint32(i).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
- (* Invariant 'Partial' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
- (* Invariant 'Range' *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: t1_0[i <- v][i_1] = v.
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Goal Loop assigns 'lack,Zone_j' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Goal Loop assigns 'lack,Zone_j' (2/3):
+Effect at line 58
Assume {
- Type: is_uint32(i).
- (* Invariant 'Partial' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
- (* Invariant 'Range' *)
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
-Prove: true.
+Goal Loop assigns 'lack,Zone_j' (3/3):
+Effect at line 59
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: j <= 20.
+}
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
+ (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 24):
+Goal Assigns 'lack' in 'init_t2_v1' (1/2):
+Effect at line 51
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (1/2):
-Effect at line 26
+Goal Assigns 'lack' in 'init_t2_v1' (2/2):
+Effect at line 51
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 51):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 51):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (2/2):
-Effect at line 26
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 58):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: j < to_uint32(1 + j).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 58):
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function init_t2
+ Function init_t2_v2
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 30) in 'init_t2':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 68) in 'init_t2_v2':
Assume {
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
(* Invariant 'Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
@@ -215,16 +1301,15 @@ Prove: t2_0[i][i_1] = v.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 77):
Let m = t2_0[i].
Assume {
Type: is_uint32(i).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
(* Invariant 'Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -233,10 +1318,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -248,18 +1332,17 @@ Prove: m[0] = t2_0[i_1][i_2].
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 77):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
Assume {
Type: is_uint32(i).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -268,10 +1351,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -283,21 +1365,20 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 83):
Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
(* Invariant 'Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
@@ -306,10 +1387,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
(* Invariant 'Previous_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
@@ -325,21 +1405,20 @@ Prove: m[j <- v][i_1] = v.
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 83):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 84):
Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
(* Invariant 'Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -348,10 +1427,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -367,18 +1445,17 @@ Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
------------------------------------------------------------
-Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 84):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
Assume {
Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -387,10 +1464,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -406,172 +1482,157 @@ Prove: to_uint32(1 + j) <= 20.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'j' (file tests/wp_typed/user_init.i, line 50):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 90):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 53):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 93):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (1/3):
+Goal Loop assigns 'tactic,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (2/3):
-Effect at line 41
+Goal Loop assigns 'tactic,Zone_i' (2/3):
+Effect at line 80
Assume {
- Type: is_uint32(i).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (t2_2[i_2][i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (3/3):
-Effect at line 47
+Goal Loop assigns 'tactic,Zone_i' (3/3):
+Effect at line 87
Assume {
- Type: is_uint32(i).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (t2_2[i_2][i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (1/3):
+Goal Loop assigns 'tactic,Zone_j' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (2/3):
-Effect at line 47
+Goal Loop assigns 'tactic,Zone_j' (2/3):
+Effect at line 87
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < j) -> (t2_2[i_2][i_5] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (3/3):
-Effect at line 48
+Goal Loop assigns 'tactic,Zone_j' (3/3):
+Effect at line 88
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: i <= 10.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -581,53 +1642,118 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
- (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (j <= i_1) /\
+ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (1/2):
-Effect at line 41
+Goal Assigns 'tactic' in 'init_t2_v2' (1/2):
+Effect at line 80
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (2/2):
-Effect at line 41
+Goal Assigns 'tactic' in 'init_t2_v2' (2/2):
+Effect at line 80
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: j < to_uint32(1 + j).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function init_t2_bis
+ Function init_t2_v3
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 57) in 'init_t2_bis':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 97) in 'init_t2_v3':
Assume {
- Type: is_sint32(v).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
}
@@ -635,261 +1761,275 @@ Prove: t2_0[i][i_1] = v.
------------------------------------------------------------
-Goal Exit-condition (file tests/wp_typed/user_init.i, line 59) in 'init_t2_bis':
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Loop assigns ... *)
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Exit Effects *)
- Have: (forall i_1 : Z. ((i_1 != i) -> (t2_2[i_1] = t2_1[i_1]))) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < 0) \/ (20 <= i_1)) -> (t2_2[i][i_1] = t2_1[i][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (v_1[i_1] = v))).
}
-Prove: false.
+Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
-Let m = t2_0[i].
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
- (* Invariant 'Partial_i' *)
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
+ (t2_1[i_4][i_3] = t2_0[i_4][i_3])))))).
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = v_1))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
- (* Call Effects *)
- Have: (forall i_3 : Z. ((i_3 != i) -> (t2_2[i_3] = t2_0[i_3]))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
- (((i_3 < 0) \/ (20 <= i_3)) -> (t2_2[i][i_3] = m[i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (v[i_3] = v_1))).
}
-Prove: m[0] = t2_0[i_1][i_2].
+Prove: t2_0[i <- v][i_1][i_2] = v[0].
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Goal Establishment of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
-Let m = t2_2[i].
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Loop assigns ... *)
+ Type: is_uint32(i_1) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (i < to_uint32(1 + j)).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i_1) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v_1))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i_1) /\ (i_1 <= 10).
+ (* Then *)
+ Have: i_1 <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (v[i_2] = v_1))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: v[j <- v_1][i] = v_1.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (m[i_1] = v))).
- (* Call Effects *)
- Have: (forall i_1 : Z. ((i_1 != i) -> (t2_1[i_1] = t2_2[i_1]))) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < 0) \/ (20 <= i_1)) -> (t2_1[i][i_1] = m[i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Prove: true.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 118):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 71):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 121):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (1/3):
+Goal Loop assigns 'lack,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (2/3):
-Effect at line 68
-Let m = t2_2[i].
+Goal Loop assigns 'lack,Zone_i' (2/3):
+Effect at line 109
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
- (* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
- (* Call Effects *)
- Have: (forall i_3 : Z. ((i_3 != i) -> (t2_1[i_3] = t2_2[i_3]))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
- (((i_3 < 0) \/ (20 <= i_3)) -> (t2_1[i][i_3] = m[i_3]))))).
+ Have: i_2 <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) -> (v_1[i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (3/3):
-Call Effect at line 69
-Let m = t2_2[i].
+Goal Loop assigns 'lack,Zone_i' (3/3):
+Effect at line 115
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
(* Invariant 'Range_i' *)
Have: i <= 10.
- (* Call 'init' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (m[i_2] = v))).
- (* Call Effects *)
- Have: (forall i_2 : Z. ((i_2 != i) -> (t2_1[i_2] = t2_2[i_2]))) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
- (((i_2 < 0) \/ (20 <= i_2)) -> (t2_1[i][i_2] = m[i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (v_1[i_2] = v))).
}
-Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
- (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
+ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_j' (1/2):
+Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/3):
-Effect at line 68
+Goal Loop assigns 'lack,Zone_j' (2/2):
+Effect at line 115
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/3):
-Effect at line 68
+Goal Assigns 'lack' in 'init_t2_v3' (1/2):
+Effect at line 109
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_v3' (2/2):
+Effect at line 109
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (3/3):
-Call Effect at line 69
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Goal *)
- When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
- Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
- (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
- Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
- ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
- Have: i <= 10.
- (* Exit Effects *)
- Have: (forall i_2 : Z. ((i_2 != i) -> (t2_2[i_2] = t2_1[i_2]))) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
- (((i_2 < 0) \/ (20 <= i_2)) -> (t2_2[i][i_2] = t2_1[i][i_2]))))).
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (v_1[i_1] = v))).
}
-Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
- (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/2):
-Effect at line 68
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/2):
-Effect at line 68
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
Assume {
- Have: 0 <= i_2.
- Have: 0 <= i_3.
- Have: i_2 <= 9.
- Have: i_3 <= 19.
- Have: 0 <= i.
- Have: 0 <= i_1.
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
- Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
- (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 1) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
-:
-Prove: true.
+Prove: j < to_uint32(1 + j).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 2) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
-:
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index fa09d25239473625ccad474d2a23e2e83bc03ada..04c72c689908f0f61a572a5cc939137d987d10ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -2,14 +2,18 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
+[wp] Computing [100 goals...]
------------------------------------------------------------
Function init
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 3) in 'init':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 10) in 'init':
Let a_1 = shift_sint32(a, 0).
Assume {
Type: is_sint32(i) /\ is_sint32(n).
@@ -31,7 +35,7 @@ Prove: havoc(Mint_undef_0, Mint_0, a_1, i)[shift_sint32(a, i_1)] = v.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 9):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 17):
Let a_1 = shift_sint32(a, 0).
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
Assume {
@@ -54,12 +58,12 @@ Prove: a_2[shift_sint32(a, i) <- v][shift_sint32(a, i_1)] = v.
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 9):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 17):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 8):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 16):
Let a_1 = shift_sint32(a, 0).
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
@@ -79,18 +83,18 @@ Prove: (-1) <= i.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 8):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 16):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 10) (1/2):
+Goal Loop assigns 'Zone' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 10) (2/2):
-Effect at line 12
+Goal Loop assigns 'Zone' (2/2):
+Effect at line 20
Let a_1 = shift_sint32(a, 0).
Let a_2 = shift_sint32(a, i).
Assume {
@@ -113,8 +117,18 @@ Prove: included(a_2, 1, a_1, n).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 4) in 'init':
-Effect at line 12
+Goal Assigns (file tests/wp_typed/user_init.i, line 9) in 'init':
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 20):
Prove: true.
------------------------------------------------------------
@@ -122,7 +136,7 @@ Prove: true.
Function init_t1
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 16) in 'init_t1':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 24) in 'init_t1':
Assume {
Type: is_uint32(i_1).
(* Goal *)
@@ -134,78 +148,1150 @@ Assume {
(* Else *)
Have: 10 <= i_1.
}
-Prove: t1_0[i] = v.
+Prove: t1_0[i] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 32):
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: t1_0[i <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 31):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 31):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'Zone':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 26) in 'init_t1' (1/2):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 26) in 'init_t1' (2/2):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 35):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 35):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis_v1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 125) in 'init_t2_bis_v1':
+Let a = global(G_t2_48).
+Assume {
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_1 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_1)))))) ->
+ (Mint_1[a_1] = Mint_0[a_1])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i_2) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Else *)
+ Have: 10 <= i_2.
+}
+Prove: Mint_0[shift_sint32(shift_A20_sint32(a, i), i_1)] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_4 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_4)))))) ->
+ (Mint_1[a_4] = Mint_0[a_4])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (a_3[shift_sint32(a_1, i_3)] = v))).
+}
+Prove: a_3[shift_sint32(shift_A20_sint32(a, i_1), i_2)] = Mint_undef_0[a_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 139):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (2/3):
+Effect at line 137
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_3)] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (3/3):
+Call Effect at line 138
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_3), i_2) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_3), i_2)] = v))))).
+ (* Invariant 'Range' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_2)] = v))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (1/3):
+Effect at line 137
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (2/3):
+Effect at line 137
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (3/3):
+Call Effect at line 138
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (1/2):
+Effect at line 137
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v1' (2/2):
+Effect at line 137
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 7) in 'init'' in 'init_t2_bis_v1' at call 'init' (file tests/wp_typed/user_init.i, line 138)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 8) in 'init'' in 'init_t2_bis_v1' at call 'init' (file tests/wp_typed/user_init.i, line 138)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis_v2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 143) in 'init_t2_bis_v2':
+Let a = global(G_t2_48).
+Assume {
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_1 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_1)))) ->
+ (Mint_1[a_1] = Mint_0[a_1])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i_2) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Else *)
+ Have: 10 <= i_2.
+}
+Prove: Mint_0[shift_sint32(shift_A20_sint32(a, i), i_1)] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 145) in 'init_t2_bis_v2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Let a_2 = shift_sint32(a_1, 0).
+Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_4 : addr.
+ ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_4)))) ->
+ (Mint_1[a_4] = Mint_0[a_4])).
+ (* Invariant 'Partial' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) ->
+ (Mint_0[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (a_3[shift_sint32(a_1, i_3)] = v))).
+}
+Prove: a_3[shift_sint32(shift_A20_sint32(a, i_1), i_2)] = Mint_undef_0[a_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 157):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (2/3):
+Effect at line 155
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i_2).
+Assume {
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_6), i_5) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_6), i_5)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_2) /\ (i_2 <= 10).
+ (* Then *)
+ Have: i_2 <= 9.
+ (* Call 'init' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_5)] = v))).
+}
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone' (3/3):
+Call Effect at line 156
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_3,i_2 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_3), i_2) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_3), i_2)] = v))))).
+ (* Invariant 'Range' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_2)] = v))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
+ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (1/3):
+Effect at line 155
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (2/3):
+Effect at line 155
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (3/3):
+Call Effect at line 156
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (1/2):
+Effect at line 155
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_bis_v2' (2/2):
+Effect at line 155
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a])).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Let a = global(G_t2_48).
+Let a_1 = shift_A20_sint32(a, i).
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns 'lack,Zone' *)
+ Have: forall a_2 : addr.
+ ((forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_2), i_1) != a_2)))) ->
+ (Mint_0[a_2] = Mint_1[a_2])).
+ (* Invariant 'Partial' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_2), i_1)] = v))))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
+ [shift_sint32(a_1, i_1)] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 7) in 'init'' in 'init_t2_bis_v2' at call 'init' (file tests/wp_typed/user_init.i, line 156)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 8) in 'init'' in 'init_t2_bis_v2' at call 'init' (file tests/wp_typed/user_init.i, line 156)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_v1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 39) in 'init_t2_v1':
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 48):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 48):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 47):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 47):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 54):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: m[j <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 54):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 55):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (m[i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 55):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 53):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 53):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 64):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_i' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_i' (2/3):
+Effect at line 51
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Goal Loop assigns 'lack,Zone_i' (3/3):
+Effect at line 58
Assume {
Type: is_uint32(i).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
- (* Invariant 'Partial' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
- (* Invariant 'Range' *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: t1_0[i <- v][i_1] = v.
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Goal Loop assigns 'lack,Zone_j' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Goal Loop assigns 'lack,Zone_j' (2/3):
+Effect at line 58
Assume {
- Type: is_uint32(i).
- (* Invariant 'Partial' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
- (* Invariant 'Range' *)
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
-Prove: true.
+Goal Loop assigns 'lack,Zone_j' (3/3):
+Effect at line 59
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: j <= 20.
+}
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
+ (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 24):
+Goal Assigns 'lack' in 'init_t2_v1' (1/2):
+Effect at line 51
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (1/2):
-Effect at line 26
+Goal Assigns 'lack' in 'init_t2_v1' (2/2):
+Effect at line 51
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 51):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 51):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (2/2):
-Effect at line 26
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 58):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'lack,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: j < to_uint32(1 + j).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 58):
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function init_t2
+ Function init_t2_v2
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 30) in 'init_t2':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 68) in 'init_t2_v2':
Assume {
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
(* Invariant 'Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
@@ -215,16 +1301,15 @@ Prove: t2_0[i][i_1] = v.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 77):
Let m = t2_0[i].
Assume {
Type: is_uint32(i).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
(* Invariant 'Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -233,10 +1318,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -248,18 +1332,17 @@ Prove: m[0] = t2_0[i_1][i_2].
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 77):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
Assume {
Type: is_uint32(i).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -268,10 +1351,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -283,21 +1365,20 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 76):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 83):
Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
(* Invariant 'Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
@@ -306,10 +1387,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
(* Invariant 'Previous_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
@@ -325,21 +1405,20 @@ Prove: m[j <- v][i_1] = v.
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 83):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 84):
Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
(* Invariant 'Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -348,10 +1427,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
(t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
@@ -367,18 +1445,17 @@ Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
------------------------------------------------------------
-Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 84):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
Assume {
Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -387,10 +1464,9 @@ Assume {
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -406,172 +1482,157 @@ Prove: to_uint32(1 + j) <= 20.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 82):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'j' (file tests/wp_typed/user_init.i, line 50):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 90):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 53):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 93):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (1/3):
+Goal Loop assigns 'tactic,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (2/3):
-Effect at line 41
+Goal Loop assigns 'tactic,Zone_i' (2/3):
+Effect at line 80
Assume {
- Type: is_uint32(i).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (t2_2[i_2][i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (3/3):
-Effect at line 47
+Goal Loop assigns 'tactic,Zone_i' (3/3):
+Effect at line 87
Assume {
- Type: is_uint32(i).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
+ (t2_2[i_2][i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (1/3):
+Goal Loop assigns 'tactic,Zone_j' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (2/3):
-Effect at line 47
+Goal Loop assigns 'tactic,Zone_j' (2/3):
+Effect at line 87
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: i_2 <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < j) -> (t2_2[i_2][i_5] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (3/3):
-Effect at line 48
+Goal Loop assigns 'tactic,Zone_j' (3/3):
+Effect at line 88
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Goal *)
When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: i <= 10.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_j' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
(* Invariant 'Previous_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
@@ -581,53 +1642,118 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
- (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (j <= i_1) /\
+ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (1/2):
-Effect at line 41
+Goal Assigns 'tactic' in 'init_t2_v2' (1/2):
+Effect at line 80
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (2/2):
-Effect at line 41
+Goal Assigns 'tactic' in 'init_t2_v2' (2/2):
+Effect at line 80
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
+ (* Loop assigns 'tactic,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: i < to_uint32(1 + i).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 80):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'tactic,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns 'tactic,Zone_j' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: j < to_uint32(1 + j).
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 87):
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function init_t2_bis
+ Function init_t2_v3
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 57) in 'init_t2_bis':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 97) in 'init_t2_v3':
Assume {
- Type: is_sint32(v).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
}
@@ -635,261 +1761,275 @@ Prove: t2_0[i][i_1] = v.
------------------------------------------------------------
-Goal Exit-condition (file tests/wp_typed/user_init.i, line 59) in 'init_t2_bis':
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Loop assigns ... *)
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Exit Effects *)
- Have: (forall i_1 : Z. ((i_1 != i) -> (t2_2[i_1] = t2_1[i_1]))) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < 0) \/ (20 <= i_1)) -> (t2_2[i][i_1] = t2_1[i][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (v_1[i_1] = v))).
}
-Prove: false.
+Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
-Let m = t2_0[i].
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
- (* Invariant 'Partial_i' *)
+ ((i_3 <= 19) -> (((i_4 < 0) \/ (10 <= i_4)) ->
+ (t2_1[i_4][i_3] = t2_0[i_4][i_3])))))).
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = v_1))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
- (* Call Effects *)
- Have: (forall i_3 : Z. ((i_3 != i) -> (t2_2[i_3] = t2_0[i_3]))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
- (((i_3 < 0) \/ (20 <= i_3)) -> (t2_2[i][i_3] = m[i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (v[i_3] = v_1))).
}
-Prove: m[0] = t2_0[i_1][i_2].
+Prove: t2_0[i <- v][i_1][i_2] = v[0].
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Goal Establishment of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
-Let m = t2_2[i].
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Loop assigns ... *)
+ Type: is_uint32(i_1) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (i < to_uint32(1 + j)).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i_1) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v_1))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i_1) /\ (i_1 <= 10).
+ (* Then *)
+ Have: i_1 <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (v[i_2] = v_1))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: v[j <- v_1][i] = v_1.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
- ((i_1 <= 19) ->
- (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
(t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (m[i_1] = v))).
- (* Call Effects *)
- Have: (forall i_1 : Z. ((i_1 != i) -> (t2_1[i_1] = t2_2[i_1]))) /\
- (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < 0) \/ (20 <= i_1)) -> (t2_1[i][i_1] = m[i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Prove: true.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 118):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 71):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 121):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (1/3):
+Goal Loop assigns 'lack,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (2/3):
-Effect at line 68
-Let m = t2_2[i].
+Goal Loop assigns 'lack,Zone_i' (2/3):
+Effect at line 109
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Have: 0 <= i.
+ Have: i <= 9.
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
- (* Loop assigns ... *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
- (* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 <= 9) ->
+ ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
+ (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_6,i_5 : Z. ((0 <= i_5) -> ((0 <= i_6) -> ((i_6 < i_2) ->
+ ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
- (* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
- (* Call Effects *)
- Have: (forall i_3 : Z. ((i_3 != i) -> (t2_1[i_3] = t2_2[i_3]))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
- (((i_3 < 0) \/ (20 <= i_3)) -> (t2_1[i][i_3] = m[i_3]))))).
+ Have: i_2 <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) -> (v_1[i_5] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
+ (0 <= i_6) /\ (i <= i_6) /\ (i_6 <= 9).
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (3/3):
-Call Effect at line 69
-Let m = t2_2[i].
+Goal Loop assigns 'lack,Zone_i' (3/3):
+Effect at line 115
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ ((i_2 <= 19) -> (((i_3 < 0) \/ (10 <= i_3)) ->
(t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
+ (* Invariant 'lack,Partial_i' *)
Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
(* Invariant 'Range_i' *)
Have: i <= 10.
- (* Call 'init' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (m[i_2] = v))).
- (* Call Effects *)
- Have: (forall i_2 : Z. ((i_2 != i) -> (t2_1[i_2] = t2_2[i_2]))) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
- (((i_2 < 0) \/ (20 <= i_2)) -> (t2_1[i][i_2] = m[i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (v_1[i_2] = v))).
}
-Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
- (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
+ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9).
+
+------------------------------------------------------------
+
+Goal Loop assigns 'lack,Zone_j' (1/2):
+Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/3):
-Effect at line 68
+Goal Loop assigns 'lack,Zone_j' (2/2):
+Effect at line 115
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/3):
-Effect at line 68
+Goal Assigns 'lack' in 'init_t2_v3' (1/2):
+Effect at line 109
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns 'lack' in 'init_t2_v3' (2/2):
+Effect at line 109
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
+ (* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ ((i_4 <= 19) -> (((i_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
+ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (3/3):
-Call Effect at line 69
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
- (* Goal *)
- When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns ... *)
- Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
- ((i_2 <= 19) ->
- (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
- (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
- (* Invariant 'Partial_i' *)
- Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
- ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ Type: is_uint32(i).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
(* Invariant 'Range_i' *)
- Have: i <= 10.
- (* Exit Effects *)
- Have: (forall i_2 : Z. ((i_2 != i) -> (t2_2[i_2] = t2_1[i_2]))) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
- (((i_2 < 0) \/ (20 <= i_2)) -> (t2_2[i][i_2] = t2_1[i][i_2]))))).
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (v_1[i_1] = v))).
}
-Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
- (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/2):
-Effect at line 68
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/2):
-Effect at line 68
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
Assume {
- Have: 0 <= i_2.
- Have: 0 <= i_3.
- Have: i_2 <= 9.
- Have: i_3 <= 19.
- Have: 0 <= i.
- Have: 0 <= i_1.
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns 'lack,Zone_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) -> (((i_2 < 0) \/ (10 <= i_2)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'lack,Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
Have: i <= 9.
- Have: i_1 <= 19.
- (* Loop assigns ... *)
- Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
- (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
}
-Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
- (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 1) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
-:
-Prove: true.
+Prove: j < to_uint32(1 + j).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 2) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
-:
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ea38a9018b48269759743504ec1c6b2338f588db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -0,0 +1,115 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
+[wp] 89 goals scheduled
+[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
+[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
+[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_init_assigns : Valid
+[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Partial_preserved : Valid
+[wp] [Qed] Goal typed_init_t1_loop_invariant_Partial_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_t1_loop_invariant_Range_established : Valid
+[wp] [Qed] Goal typed_init_t1_loop_assigns : Valid
+[wp] [Qed] Goal typed_init_t1_assigns_part1 : Valid
+[wp] [Qed] Goal typed_init_t1_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t1_loop_variant_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_ensures : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_exits : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_invariant_Partial_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_loop_invariant_Partial_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_loop_invariant_Range_established : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_assert_Offset : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_loop_variant_positive : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_call_init_requires : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_call_init_requires_2 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_ensures : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_exits : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_invariant_Partial_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_loop_invariant_Partial_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_loop_invariant_Range_established : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_assert_Offset_i : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_loop_variant_positive : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires_2 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Partial_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Partial_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Range_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Range_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Partial_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Partial_j_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Previous_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Previous_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_invariant_Range_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_invariant_Range_j_established : Valid
+[wp] [Qed] Goal typed_init_t2_v1_assert_Last_j : Valid
+[wp] [Qed] Goal typed_init_t2_v1_assert_Last_i : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_variant_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_variant_2_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v1_loop_variant_2_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Partial_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Partial_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Range_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Range_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Partial_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Partial_j_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Previous_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Previous_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_invariant_Range_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_invariant_Range_j_established : Valid
+[wp] [Qed] Goal typed_init_t2_v2_assert_Last_j : Valid
+[wp] [Qed] Goal typed_init_t2_v2_assert_Last_i : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_variant_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v2_loop_variant_2_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_variant_2_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Range_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Range_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Partial_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Partial_j_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_Range_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Range_j_established : Valid
+[wp] [Qed] Goal typed_init_t2_v3_assert_Last_j : Valid
+[wp] [Qed] Goal typed_init_t2_v3_assert_Last_i : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_variant_positive : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_variant_2_decrease : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_variant_2_positive : Valid
+[wp] Proved goals: 89 / 89
+ Qed: 51
+ Alt-Ergo: 38
+[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json'
+[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+init 6 4 (80..104) 10 100%
+init_t1 6 4 (12..24) 10 100%
+init_t2_v1 9 8 (40..52) 17 100%
+init_t2_v2 9 8 (32..44) 17 100%
+init_t2_v3 7 6 (16..28) 13 100%
+init_t2_bis_v1 7 4 (208..256) 11 100%
+init_t2_bis_v2 7 4 (192..240) 11 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..77c6f534fe60db839cc484b83d6813f8a08e9ec3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -0,0 +1,32 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
+[wp] 8 goals scheduled
+[wp] [Qed] Goal typed_init_t2_v2_loop_assigns_part1 : Valid
+[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session/test-1'
+[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session/test-1/wp'
+[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_part2 : Valid
+[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_init_t2_v2_loop_assigns_2_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_2_part2 : Valid
+[wp] [Tactical] Goal typed_init_t2_v2_loop_assigns_2_part3 : Valid
+[wp] [Tactical] Goal typed_init_t2_v2_assigns_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_v2_assigns_part2 : Valid
+[wp] Proved goals: 8 / 8
+ Qed: 3
+ Alt-Ergo: 0 (unsuccess: 5)
+ Script: 5
+[wp] Updated session with 5 new valid scripts.
+[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.1.report.json'
+[wp] Report out: 'tests/wp_typed/result_qualif/user_init.1.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+init_t2_v2 3 - (16..28) 8 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..910fde6d48cbcda64616291ac7655ebc422d64ad
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -0,0 +1,56 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 300 [...]
+[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
+[wp] 33 goals scheduled
+[wp] [Qed] Goal typed_init_t2_bis_v1_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_exit_part2 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part3 : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_normal_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_normal_part2 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_assigns_exit_part2 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part3 : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_normal_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_v2_assigns_normal_part2 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_v1_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_v1_loop_assigns_2_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_2_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_loop_assigns_2_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_v1_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v1_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_invariant_lack_Partial_i_preserved : Unsuccess
+[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_lack_Partial_i_established : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_2_part1 : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_2_part2 : Valid
+[wp] [Qed] Goal typed_init_t2_v3_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_v3_assigns_part2 : Unsuccess
+[wp] Proved goals: 16 / 33
+ Qed: 16
+ Alt-Ergo: 0 (unsuccess: 17)
+[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.2.report.json'
+[wp] Report out: 'tests/wp_typed/result_qualif/user_init.2.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+init_t2_v1 3 - 8 37.5%
+init_t2_v3 5 - 9 55.6%
+init_t2_bis_v1 4 - 8 50.0%
+init_t2_bis_v2 4 - 8 50.0%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
deleted file mode 100644
index 4166c7752ea435cbbd58ec6de2eb69e962fda690..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
+++ /dev/null
@@ -1,74 +0,0 @@
-# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] 54 goals scheduled
-[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_init_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_init_t1_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Partial_preserved : Valid
-[wp] [Qed] Goal typed_init_t1_loop_invariant_Partial_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Range_preserved : Valid
-[wp] [Qed] Goal typed_init_t1_loop_invariant_Range_established : Valid
-[wp] [Qed] Goal typed_init_t1_loop_assigns : Valid
-[wp] [Qed] Goal typed_init_t1_assigns_part1 : Valid
-[wp] [Qed] Goal typed_init_t1_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Partial_i_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_loop_invariant_Partial_i_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Range_i_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_loop_invariant_Range_i_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Partial_j_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_loop_invariant_Partial_j_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Previous_i_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_loop_invariant_Previous_i_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Range_j_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_loop_invariant_Range_j_established : Valid
-[wp] [Qed] Goal typed_init_t2_assert_j : Valid
-[wp] [Qed] Goal typed_init_t2_assert_i : Valid
-[wp] [Qed] Goal typed_init_t2_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_part2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_part3 : Unsuccess
-[wp] [Qed] Goal typed_init_t2_loop_assigns_2_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_2_part2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_2_part3 : Unsuccess
-[wp] [Qed] Goal typed_init_t2_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_assigns_part2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_exits : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_invariant_Partial_i_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_bis_loop_invariant_Partial_i_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_invariant_Range_i_preserved : Valid
-[wp] [Qed] Goal typed_init_t2_bis_loop_invariant_Range_i_established : Valid
-[wp] [Qed] Goal typed_init_t2_bis_assert_i : Valid
-[wp] [Qed] Goal typed_init_t2_bis_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_assigns_part2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_assigns_part3 : Unsuccess
-[wp] [Qed] Goal typed_init_t2_bis_assigns_exit_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_exit_part2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_exit_part3 : Unsuccess
-[wp] [Qed] Goal typed_init_t2_bis_assigns_normal_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_normal_part2 : Unsuccess
-[wp] [Qed] Goal typed_init_t2_bis_call_init_requires : Valid
-[wp] [Qed] Goal typed_init_t2_bis_call_init_requires_2 : Valid
-[wp] Proved goals: 43 / 54
- Qed: 27
- Alt-Ergo: 16 (unsuccess: 11)
-[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json'
-[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-init 4 4 (80..104) 8 100%
-init_t1 5 3 (12..24) 8 100%
-init_t2 10 6 (40..52) 21 76.2%
-init_t2_bis 8 3 (36..48) 17 64.7%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index 416a94e97e0218b9208fb26cd197e6378be32cce..06f597c3d3afa822390bdfef4da9bf41a3b104c4 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,13 +1,21 @@
+/* run.config_qualif
+ EXECNOW: rm -rf @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session/
+ OPT: -wp-prop=-lack,-tactic
+ OPT: -wp-prop=tactic -wp-auto=wp:split -session @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session/test-@PTEST_NUMBER@
+ OPT: -wp-prop=lack -wp-steps 300
+ */
/*@ requires \valid(a+(0..n-1)) ;
@ requires n >= 0 ;
- @ ensures \forall int k ; 0 <= k < n ==> a[k] == v ;
@ assigns a[0..n-1] ;
+ @ ensures \forall int k ; 0 <= k < n ==> a[k] == v ;
+ @ exits \false;
*/
void init( int * a , int n , int v )
{
- /*@ loop invariant Range: 0 <= i <= n ;
+ /*@ loop assigns Zone: i,a[0..n-1] ;
+ @ loop invariant Range: 0 <= i <= n ;
@ loop invariant Partial: \forall int k ; 0 <= k < i ==> a[k] == v ;
- @ loop assigns i,a[0..n-1] ;
+ @ loop variant Decr_i: n - i ;
*/
for (int i = 0 ; i < n ; i++) a[i] = v ;
}
@@ -19,9 +27,10 @@ int t1[10];
*/
void init_t1(int v) {
unsigned i;
- /*@ loop invariant Range: 0 <= i <= 10 ;
+ /*@ loop assigns Zone: i,t1[0..9] ;
+ @ loop invariant Range: 0 <= i <= 10 ;
@ loop invariant Partial: \forall integer k ; 0 <= k < i ==> t1[k] ≡ v ;
- @ loop assigns i,t1[0..9] ;
+ @ loop variant Decr: 10 - i ;
*/
for (i = 0 ; i < 10 ; i++) t1[i] = v ;
}
@@ -29,45 +38,123 @@ void init_t1(int v) {
int t2[10][20];
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
@ exits \false;
- @ assigns t2[0..9][0..19];
+ @ assigns lack: t2[0..9][0..19];
*/
-void init_t2(int v) {
+void init_t2_v1(int v) {
unsigned i,j;
- /*@ loop assigns i, j, t2[0..9][0..19];
+ /*@ loop assigns lack: Zone_i: i, j, t2[0..9][0..19];
@ loop invariant Range_i: 0 <= i <= 10 ;
@ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
- */
+ @ loop variant Decr_i: 10 - i ;
+ */
for(i = 0; i <= 9; i++) {
- /*@ loop assigns j, t2[0..9][0..19];
+ /*@ loop assigns lack: Zone_j: j, t2[0..9][0..19];
@ loop invariant Range_j: 0 <= j <= 20 ;
@ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
@ loop invariant Previous_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == \at(t2[k][l], LoopEntry);
+ @ loop variant Decr_j: 20 - j ;
*/
for(j = 0; j <= 19; j++) {
t2[i][j] = v;
}
- //@ assert j: j==20;
+ //@ assert Last_j: j==20;
;
}
- //@ assert i: i==10;
+ //@ assert Last_i: i==10;
;
}
//-------------------------
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
- @ assigns t2[0..9][0..19];
@ exits \false;
+ @ assigns tactic: t2[..][..];
*/
-void init_t2_bis(int v) {
+void init_t2_v2(int v) {
- unsigned i;
- /*@ loop assigns i, t2[0..9][0..19];
+ unsigned i,j;
+ /*@ loop assigns tactic: Zone_i: i, j, t2[..][..];
@ loop invariant Range_i: 0 <= i <= 10 ;
@ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ @ loop variant Decr_i: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
- init(&t2[i][0], 20, v);
+ /*@ loop assigns tactic: Zone_j: j, t2[..][..];
+ @ loop invariant Range_j: 0 <= j <= 20 ;
+ @ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
+ @ loop invariant Previous_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == \at(t2[k][l], LoopEntry);
+ @ loop variant Decr_j: 20 - j ;
+ */
+ for(j = 0; j <= 19; j++) {
+ t2[i][j] = v;
+ }
+ //@ assert Last_j: j==20;
+ ;
}
- //@ assert i: i==10;
+ //@ assert Last_i: i==10;
;
}
+//-------------------------
+/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+ @ exits \false;
+ @ assigns lack: t2[..][..];
+ */
+void init_t2_v3(int v) {
+
+ unsigned i,j;
+ /*@ loop assigns lack: Zone_i: i, j, t2[..][..];
+ @ loop invariant Range_i: 0 <= i <= 10 ;
+ @ loop invariant lack: Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ @ loop variant V_i: 10 - i ;
+ */
+ for(i = 0; i <= 9; i++) {
+ /*@ loop assigns lack: Zone_j: j, t2[i][..];
+ @ loop invariant Range_j: 0 <= j <= 20 ;
+ @ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
+ @ loop variant Decr_j: 20 - j ;
+ */
+ for(j = 0; j <= 19; j++) {
+ t2[i][j] = v;
+ }
+ //@ assert Last_j: j==20;
+ ;
+ }
+ //@ assert Last_i: i==10;
+ ;
+}
+//-------------------------
+/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+ @ assigns lack: t2[0..9][0..19];
+ @ exits \false;
+ */
+void init_t2_bis_v1(int v) {
+
+ unsigned i;
+ /*@ loop assigns lack: Zone: i, t2[0..9][0..19];
+ @ loop invariant Range: 0 <= i <= 10 ;
+ @ loop invariant Partial: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ @ loop variant Decr: 10 - i ;
+ */
+ for(i = 0; i <= 9; i++) {
+ init(&t2[i][0], 20, v);
+ //@ assert Offset: &t2[i][0] == &t2[0][0] + 20*i;
+ }
+}
+//-------------------------
+/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+ @ assigns lack: t2[..][..];
+ @ exits \false;
+ */
+void init_t2_bis_v2(int v) {
+
+ unsigned i;
+ /*@ loop assigns lack: Zone: i, t2[..][..];
+ @ loop invariant Range: 0 <= i <= 10 ;
+ @ loop invariant Partial: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ @ loop variant Decr: 10 - i ;
+ */
+ for(i = 0; i <= 9; i++) {
+ init(&t2[i][0], 20, v);
+ //@ assert Offset_i: &t2[i][0] == &t2[0][0] + 20*i;
+ ;
+ }
+}