Skip to content
Snippets Groups Projects
Commit 424bba0b authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[WP/test] adding a test initializing multidimentianal arrays

parent 57c8e509
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3268 additions and 772 deletions
src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+ 1480
− 340
View file @ 424bba0b
......@@ -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.
------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+ 1480
− 340
View file @ 424bba0b
......@@ -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.
------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle 0 → 100644
+ 115
− 0
View file @ 424bba0b
# 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%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle 0 → 100644
+ 32
− 0
View file @ 424bba0b
# 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%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle 0 → 100644
+ 56
− 0
View file @ 424bba0b
# 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%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle deleted 100644 → 0
+ 0
− 74
View file @ 57c8e509
# 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%
-------------------------------------------------------------
src/plugins/wp/tests/wp_typed/user_init.i
+ 105
− 18
View file @ 424bba0b
/* 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;
;
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment