From 509f2b79ab847ebce4a7b700fa6f43d20a863ffa Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 1 Mar 2019 10:11:03 +0100
Subject: [PATCH] [WP/test] adding a test initializing multidimentianal arrays
---
.../wp_typed/oracle/user_init.0.res.oracle | 345 ++++++++++--------
.../wp_typed/oracle/user_init.1.res.oracle | 345 ++++++++++--------
.../oracle_qualif/user_init.0.res.oracle | 12 +-
.../oracle_qualif/user_init.1.res.oracle | 33 +-
.../oracle_qualif/user_init.2.res.oracle | 27 +-
src/plugins/wp/tests/wp_typed/user_init.i | 22 +-
6 files changed, 416 insertions(+), 368 deletions(-)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 3981469580e..86999a74131 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -231,7 +231,7 @@ Prove: true.
Function init_t2_bis_v1
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 125) in 'init_t2_bis_v1':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
Let a = global(G_t2_48).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
@@ -256,12 +256,12 @@ 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':
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 129) in 'init_t2_bis_v1':
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
@@ -292,12 +292,12 @@ 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):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -325,12 +325,12 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 139):
+Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 141):
Prove: true.
------------------------------------------------------------
@@ -341,7 +341,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'lack,Zone' (2/3):
-Effect at line 137
+Effect at line 139
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -378,7 +378,7 @@ Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
------------------------------------------------------------
Goal Loop assigns 'lack,Zone' (3/3):
-Call Effect at line 138
+Call Effect at line 140
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -408,13 +408,13 @@ Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (1/3):
-Effect at line 137
+Effect at line 139
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (2/3):
-Effect at line 137
+Effect at line 139
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -437,19 +437,19 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (3/3):
-Call Effect at line 138
+Call Effect at line 140
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (1/2):
-Effect at line 137
+Effect at line 139
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (2/2):
-Effect at line 137
+Effect at line 139
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -471,7 +471,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -499,18 +499,18 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
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)
+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 140)
:
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)
+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 140)
:
Prove: true.
@@ -519,13 +519,13 @@ Prove: true.
Function init_t2_bis_v2
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 143) in 'init_t2_bis_v2':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 145) 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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -543,12 +543,12 @@ 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':
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 147) in 'init_t2_bis_v2':
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
@@ -557,7 +557,7 @@ 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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -578,17 +578,17 @@ 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):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -610,23 +610,23 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 157):
+Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 159):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (1/3):
+Goal Loop assigns 'tactic,Zone' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (2/3):
-Effect at line 155
+Goal Loop assigns 'tactic,Zone' (2/3):
+Effect at line 157
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i_2).
Assume {
@@ -635,7 +635,7 @@ Assume {
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -658,15 +658,15 @@ Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (3/3):
-Call Effect at line 156
+Goal Loop assigns 'tactic,Zone' (3/3):
+Call Effect at line 158
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -687,14 +687,14 @@ Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (1/3):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (1/3):
+Effect at line 157
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (2/3):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (2/3):
+Effect at line 157
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -702,7 +702,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -713,20 +713,20 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (3/3):
-Call Effect at line 156
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (3/3):
+Call Effect at line 158
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (1/2):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (1/2):
+Effect at line 157
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (2/2):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (2/2):
+Effect at line 157
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -734,7 +734,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -745,12 +745,12 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -772,18 +772,18 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
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)
+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 158)
:
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)
+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 158)
:
Prove: true.
@@ -1745,124 +1745,143 @@ Prove: true.
Function init_t2_v3
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 97) in 'init_t2_v3':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 99) in 'init_t2_v3':
Assume {
+ Type: is_sint32(v).
(* 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_3 < 0) \/ (10 <= i_3)) ->
- (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
- (* 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))))).
+ When: (0 <= i) /\ (i <= 9).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
+ P_MemSet20(t2_0[i_1], 20, v))).
}
-Prove: t2_0[i][i_1] = v.
+Prove: P_MemSet20(t2_0[i], 20, v).
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
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_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))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i]).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* 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_3 < 0) \/ (10 <= i_3)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ P_MemSet20(t2_0[i_2], 20, v_1))).
(* Invariant 'Range_i' *)
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))).
+ Have: P_MemSet20(v, 20, v_1).
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: P_MemSet20(t2_0[i <- v][i_1], 20, v_1).
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
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_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_0[i_4][i_3] = v_1))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (v[i_3] = v_1))).
+ Have: P_MemSet20(v, 20, v_1).
}
-Prove: t2_0[i <- v][i_1][i_2] = v[0].
+Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
+Let m = v[j <- v_1].
Assume {
- 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))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
- Have: (0 <= i_1) /\ (i_1 <= 10).
+ Have: (0 <= i) /\ (i <= 10).
(* Then *)
- Have: i_1 <= 9.
+ Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (v[i_2] = v_1))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: v[j <- v_1][i] = v_1.
+Prove: P_MemSet20(m, to_uint32(1 + j), v_1).
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
-Prove: true.
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: P_MemSet20(m, 0, v).
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
@@ -1872,95 +1891,97 @@ Prove: to_uint32(1 + j) <= 20.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 118):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 120):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 121):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 123):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_i' (1/3):
+Goal Loop assigns 'tactic,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_i' (2/3):
-Effect at line 109
+Goal Loop assigns 'tactic,Zone_i' (2/3):
+Effect at line 111
Assume {
Have: 0 <= i.
Have: i <= 9.
- Type: is_uint32(i_2).
+ Type: IsArray1_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i_2]).
(* Goal *)
When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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 '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))))).
+ (t2_1[i_6][i_5] = t2_0[i_6][i_5])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
+ P_MemSet20(t2_0[i_5], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) -> (v_1[i_5] = v))).
+ Have: P_MemSet20(v, 20, v_1).
}
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_i' (3/3):
-Effect at line 115
+Goal Loop assigns 'tactic,Zone_i' (3/3):
+Effect at line 117
Assume {
- Type: is_uint32(i).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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_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) ->
- ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ P_MemSet20(t2_0[i_2], 20, v_1))).
(* Invariant 'Range_i' *)
Have: i <= 10.
(* Invariant 'Partial_j' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (v_1[i_2] = v))).
+ Have: P_MemSet20(v, 20, v_1).
}
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):
+Goal Loop assigns 'tactic,Zone_j' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_j' (2/2):
-Effect at line 115
+Goal Loop assigns 'tactic,Zone_j' (2/2):
+Effect at line 117
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_v3' (1/2):
-Effect at line 109
+Goal Assigns 'tactic' in 'init_t2_v3' (1/2):
+Effect at line 111
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_v3' (2/2):
-Effect at line 109
+Goal Assigns 'tactic' in 'init_t2_v3' (2/2):
+Effect at line 111
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -1968,7 +1989,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
@@ -1978,48 +1999,50 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Assume {
- Type: is_uint32(i).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
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))).
+ Have: P_MemSet20(v, 20, v_1).
}
Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
@@ -2029,7 +2052,7 @@ Prove: j < to_uint32(1 + j).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 04c72c68990..847496eab27 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -231,7 +231,7 @@ Prove: true.
Function init_t2_bis_v1
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 125) in 'init_t2_bis_v1':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
Let a = global(G_t2_48).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
@@ -256,12 +256,12 @@ 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':
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 129) in 'init_t2_bis_v1':
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 134):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
@@ -292,12 +292,12 @@ 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):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -325,12 +325,12 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 133):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 139):
+Goal Assertion 'Offset' (file tests/wp_typed/user_init.i, line 141):
Prove: true.
------------------------------------------------------------
@@ -341,7 +341,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'lack,Zone' (2/3):
-Effect at line 137
+Effect at line 139
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -378,7 +378,7 @@ Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
------------------------------------------------------------
Goal Loop assigns 'lack,Zone' (3/3):
-Call Effect at line 138
+Call Effect at line 140
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -408,13 +408,13 @@ Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (1/3):
-Effect at line 137
+Effect at line 139
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (2/3):
-Effect at line 137
+Effect at line 139
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -437,19 +437,19 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (3/3):
-Call Effect at line 138
+Call Effect at line 140
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (1/2):
-Effect at line 137
+Effect at line 139
Prove: true.
------------------------------------------------------------
Goal Assigns 'lack' in 'init_t2_bis_v1' (2/2):
-Effect at line 137
+Effect at line 139
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -471,7 +471,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Assume {
@@ -499,18 +499,18 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 137):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
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)
+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 140)
:
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)
+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 140)
:
Prove: true.
@@ -519,13 +519,13 @@ Prove: true.
Function init_t2_bis_v2
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 143) in 'init_t2_bis_v2':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 145) 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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -543,12 +543,12 @@ 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':
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 147) in 'init_t2_bis_v2':
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 152):
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
@@ -557,7 +557,7 @@ 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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -578,17 +578,17 @@ 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):
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -610,23 +610,23 @@ Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 151):
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 157):
+Goal Assertion 'Offset_i' (file tests/wp_typed/user_init.i, line 159):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (1/3):
+Goal Loop assigns 'tactic,Zone' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (2/3):
-Effect at line 155
+Goal Loop assigns 'tactic,Zone' (2/3):
+Effect at line 157
Let a = global(G_t2_48).
Let a_1 = shift_A20_sint32(a, i_2).
Assume {
@@ -635,7 +635,7 @@ Assume {
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -658,15 +658,15 @@ Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone' (3/3):
-Call Effect at line 156
+Goal Loop assigns 'tactic,Zone' (3/3):
+Call Effect at line 158
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -687,14 +687,14 @@ Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (i_1 <= i_2) /\
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (1/3):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (1/3):
+Effect at line 157
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (2/3):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (2/3):
+Effect at line 157
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -702,7 +702,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -713,20 +713,20 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (3/3):
-Call Effect at line 156
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (3/3):
+Call Effect at line 158
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (1/2):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (1/2):
+Effect at line 157
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_bis_v2' (2/2):
-Effect at line 155
+Goal Assigns 'tactic' in 'init_t2_bis_v2' (2/2):
+Effect at line 157
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -734,7 +734,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -745,12 +745,12 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
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' *)
+ (* Loop assigns 'tactic,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)))) ->
@@ -772,18 +772,18 @@ Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 155):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
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)
+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 158)
:
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)
+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 158)
:
Prove: true.
@@ -1745,124 +1745,143 @@ Prove: true.
Function init_t2_v3
------------------------------------------------------------
-Goal Post-condition (file tests/wp_typed/user_init.i, line 97) in 'init_t2_v3':
+Goal Post-condition (file tests/wp_typed/user_init.i, line 99) in 'init_t2_v3':
Assume {
+ Type: is_sint32(v).
(* 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_3 < 0) \/ (10 <= i_3)) ->
- (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
- (* 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))))).
+ When: (0 <= i) /\ (i <= 9).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
+ P_MemSet20(t2_0[i_1], 20, v))).
}
-Prove: t2_0[i][i_1] = v.
+Prove: P_MemSet20(t2_0[i], 20, v).
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
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_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))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i]).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* 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_3 < 0) \/ (10 <= i_3)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ P_MemSet20(t2_0[i_2], 20, v_1))).
(* Invariant 'Range_i' *)
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))).
+ Have: P_MemSet20(v, 20, v_1).
}
-Prove: to_uint32(1 + i) <= 10.
+Prove: P_MemSet20(t2_0[i <- v][i_1], 20, v_1).
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 105):
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
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_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_0[i_4][i_3] = v_1))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (v[i_3] = v_1))).
+ Have: P_MemSet20(v, 20, v_1).
}
-Prove: t2_0[i <- v][i_1][i_2] = v[0].
+Prove: to_uint32(1 + i) <= 10.
------------------------------------------------------------
-Goal Establishment of Invariant 'lack,Partial_i' (file tests/wp_typed/user_init.i, line 106):
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
+Let m = v[j <- v_1].
Assume {
- 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))))).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
- Have: (0 <= i_1) /\ (i_1 <= 10).
+ Have: (0 <= i) /\ (i <= 10).
(* Then *)
- Have: i_1 <= 9.
+ Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (v[i_2] = v_1))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: v[j <- v_1][i] = v_1.
+Prove: P_MemSet20(m, to_uint32(1 + j), v_1).
------------------------------------------------------------
-Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 112):
-Prove: true.
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
+ (* 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_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: P_MemSet20(m, 0, v).
------------------------------------------------------------
-Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
@@ -1872,95 +1891,97 @@ Prove: to_uint32(1 + j) <= 20.
------------------------------------------------------------
-Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 111):
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 118):
+Goal Assertion 'Last_j' (file tests/wp_typed/user_init.i, line 120):
Prove: true.
------------------------------------------------------------
-Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 121):
+Goal Assertion 'Last_i' (file tests/wp_typed/user_init.i, line 123):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_i' (1/3):
+Goal Loop assigns 'tactic,Zone_i' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_i' (2/3):
-Effect at line 109
+Goal Loop assigns 'tactic,Zone_i' (2/3):
+Effect at line 111
Assume {
Have: 0 <= i.
Have: i <= 9.
- Type: is_uint32(i_2).
+ Type: IsArray1_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i_2]).
(* Goal *)
When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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 '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))))).
+ (t2_1[i_6][i_5] = t2_0[i_6][i_5])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
+ P_MemSet20(t2_0[i_5], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) -> (v_1[i_5] = v))).
+ Have: P_MemSet20(v, 20, v_1).
}
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_i' (3/3):
-Effect at line 115
+Goal Loop assigns 'tactic,Zone_i' (3/3):
+Effect at line 117
Assume {
- Type: is_uint32(i).
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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_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) ->
- ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ P_MemSet20(t2_0[i_2], 20, v_1))).
(* Invariant 'Range_i' *)
Have: i <= 10.
(* Invariant 'Partial_j' *)
- Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (v_1[i_2] = v))).
+ Have: P_MemSet20(v, 20, v_1).
}
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):
+Goal Loop assigns 'tactic,Zone_j' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns 'lack,Zone_j' (2/2):
-Effect at line 115
+Goal Loop assigns 'tactic,Zone_j' (2/2):
+Effect at line 117
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_v3' (1/2):
-Effect at line 109
+Goal Assigns 'tactic' in 'init_t2_v3' (1/2):
+Effect at line 111
Prove: true.
------------------------------------------------------------
-Goal Assigns 'lack' in 'init_t2_v3' (2/2):
-Effect at line 109
+Goal Assigns 'tactic' in 'init_t2_v3' (2/2):
+Effect at line 111
Assume {
Have: 0 <= i_2.
Have: 0 <= i_3.
@@ -1968,7 +1989,7 @@ Assume {
Have: i_3 <= 19.
Have: 0 <= i.
Have: i <= 9.
- (* Loop assigns 'lack,Zone_i' *)
+ (* 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_5 < 0) \/ (10 <= i_5)) ->
(t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
@@ -1978,48 +1999,50 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Assume {
- Type: is_uint32(i).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
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))).
+ Have: P_MemSet20(v, 20, v_1).
}
Prove: i < to_uint32(1 + i).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 109):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
+Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
- (* Loop assigns 'lack,Zone_i' *)
+ Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray1_sint32(t2_0[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 '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))))).
+ (t2_1[i_2][i_1] = t2_0[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ P_MemSet20(t2_0[i_1], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Invariant 'Partial_j' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (v_1[i_1] = v))).
+ Have: P_MemSet20(v, j, v_1).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
@@ -2029,7 +2052,7 @@ Prove: j < to_uint32(1 + j).
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 115):
+Goal Positivity of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index ea38a9018b4..476ee7df2e4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -8,7 +8,7 @@
[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] 91 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
@@ -86,10 +86,12 @@
[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_Partial_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_invariant_Partial_i_established : 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_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
@@ -98,9 +100,9 @@
[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
+[wp] Proved goals: 91 / 91
Qed: 51
- Alt-Ergo: 38
+ Alt-Ergo: 40
[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'
-------------------------------------------------------------
@@ -109,7 +111,7 @@ 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_v3 7 8 (28..40) 15 100%
init_t2_bis_v1 7 4 (208..256) 11 100%
init_t2_bis_v2 7 4 (192..240) 11 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 77c6f534fe6..ef5a6f0f00a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -8,10 +8,18 @@
[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] 23 goals scheduled
+[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
+[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1'
+[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1/wp'
+[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Valid
+[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Valid
+[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part2 : Valid
+[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part3 : Valid
+[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_normal_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_normal_part2 : Valid
[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
@@ -19,14 +27,23 @@
[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] [Qed] Goal typed_init_t2_v3_loop_assigns_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_part2 : Valid
+[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_init_t2_v3_loop_assigns_2_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_v3_loop_assigns_2_part2 : Valid
+[wp] [Tactical] Goal typed_init_t2_v3_assigns_part1 : Valid
+[wp] [Tactical] Goal typed_init_t2_v3_assigns_part2 : Valid
+[wp] Proved goals: 23 / 23
+ Qed: 11
+ Alt-Ergo: 0 (unsuccess: 12)
+ Script: 12
+[wp] Updated session with 12 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%
+init_t2_v3 4 - (20..32) 7 100%
+init_t2_bis_v2 4 - (28..40) 8 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 910fde6d48c..17ce10c2bdd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -8,7 +8,7 @@
[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] 16 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
@@ -17,14 +17,6 @@
[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
@@ -33,24 +25,13 @@
[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] Proved goals: 7 / 16
+ Qed: 7
+ Alt-Ergo: 0 (unsuccess: 9)
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.2.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.2.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v1 3 - 8 37.5%
-init_t2_v3 5 - 9 55.6%
init_t2_bis_v1 4 - 8 50.0%
-init_t2_bis_v2 4 - 8 50.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index 06f597c3d3a..a34d4664bb4 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- EXECNOW: rm -rf @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session/
+ EXECNOW: rm -rf @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-1/
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=tactic -wp-auto=wp:split -session @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-@PTEST_NUMBER@
OPT: -wp-prop=lack -wp-steps 300
*/
/*@ requires \valid(a+(0..n-1)) ;
@@ -94,22 +94,24 @@ void init_t2_v2(int v) {
;
}
//-------------------------
-/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+//@ predicate MemSet20(int t2[20], integer n, integer v) = n <= 20 && \forall integer k ; 0 <= k < n ==> t2[k] == v;
+
+/*@ ensures \forall integer k; 0 <= k < 10 ==> MemSet20(t2[k], 20, v);
@ exits \false;
- @ assigns lack: t2[..][..];
+ @ assigns tactic: t2[..][..];
*/
void init_t2_v3(int v) {
unsigned i,j;
- /*@ loop assigns lack: Zone_i: i, j, t2[..][..];
+ /*@ loop assigns tactic: 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 invariant Partial_i: \forall integer k; 0 <= k < i ==> MemSet20(t2[k], 20, v);
@ loop variant V_i: 10 - i ;
*/
for(i = 0; i <= 9; i++) {
- /*@ loop assigns lack: Zone_j: j, t2[i][..];
+ /*@ loop assigns tactic: 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 invariant Partial_j: MemSet20(t2[i], j, v);
@ loop variant Decr_j: 20 - j ;
*/
for(j = 0; j <= 19; j++) {
@@ -141,13 +143,13 @@ void init_t2_bis_v1(int v) {
}
//-------------------------
/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
- @ assigns lack: t2[..][..];
+ @ assigns tactic: t2[..][..];
@ exits \false;
*/
void init_t2_bis_v2(int v) {
unsigned i;
- /*@ loop assigns lack: Zone: i, t2[..][..];
+ /*@ loop assigns tactic: 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 ;
--
GitLab