From 68a58d78dd0ada532495b9c0656699350a8096f3 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 26 Jun 2019 16:50:19 +0200
Subject: [PATCH] [wp] improves forall_intro
---
src/plugins/wp/Conditions.ml | 7 +
.../wp_acsl/oracle_qualif/cnf.res.oracle | 24 +-
.../wp/tests/wp_bts/oracle/ex5.res.oracle | 2 +-
.../frama_c_hashtbl_solved.res.oracle | 2 +-
.../wp_typed/oracle/user_init.0.res.oracle | 313 +++++++++---------
.../wp_typed/oracle/user_init.1.res.oracle | 313 +++++++++---------
.../oracle_qualif/user_init.1.res.oracle | 2 +-
7 files changed, 319 insertions(+), 344 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 554c893ef65..bad92bae2ea 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -478,6 +478,13 @@ let rec forall_intro p =
let hs = exist_intros hs in
let hp,p = forall_intro p in
hs @ hp , p
+ | Or qs -> (* analogy with Imply *)
+ let hps,ps = List.fold_left (fun (hs,ps) q ->
+ let hp,p = forall_intro q in (* q <==> (hp ==> p) *)
+ (hp @ hs), (p::ps)) ([],[]) qs
+ in (* ORs qs <==> ORs (hps ==> ps)
+ <==> ((ANDs hps) ==> ORs ps) *)
+ hps, (p_disj ps)
| _ -> [] , p
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 7f42f9cb837..e24296dd15a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -29,14 +29,12 @@
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B1 \/ P_B2 \/ P_C)
[wp] [Alt-Ergo] Goal typed_f_ensures_a6 : Valid
[wp:cnf]
- CNF=((not P_A) \/ (not P_A1) \/ P_A2 \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B1) \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ P_B2 \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ (not P_B1) \/ P_B2)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ (not P_B1) \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B) \/ P_B2 \/ P_C)
- /\ ((not P_A) \/ (not P_A1) \/ P_A2 \/ (not P_B1) \/ P_B2 \/ P_C)
+ CNF=(P_A2 \/ P_C) /\ (P_A2 \/ (not P_B) \/ P_C)
+ /\ (P_A2 \/ (not P_B1) \/ P_C) /\ (P_A2 \/ P_B2 \/ P_C)
+ /\ (P_A2 \/ (not P_B) \/ (not P_B1) \/ P_B2)
+ /\ (P_A2 \/ (not P_B) \/ (not P_B1) \/ P_C)
+ /\ (P_A2 \/ (not P_B) \/ P_B2 \/ P_C)
+ /\ (P_A2 \/ (not P_B1) \/ P_B2 \/ P_C)
[wp] [Alt-Ergo] Goal typed_f_ensures_a7 : Valid
[wp:cnf]
CNF=((not P_A1) \/ P_A2 \/ P_C) /\ (P_A1 \/ (not P_A2) \/ P_C)
@@ -145,8 +143,8 @@
[wp] [Alt-Ergo] Goal typed_f_ensures_c0 : Valid
[wp:cnf] CNF=P_B \/ P_B1 \/ P_B2 \/ P_C
[wp] [Qed] Goal typed_f_ensures_c1 : Valid
-[wp:cnf] CNF=(not P_B) \/ (not P_B1) \/ P_B2 \/ P_C
-[wp] [Alt-Ergo] Goal typed_f_ensures_c2 : Valid
+[wp:cnf] CNF=P_B2 \/ P_C
+[wp] [Qed] Goal typed_f_ensures_c2 : Valid
[wp:cnf] CNF=((not P_B1) \/ P_B2 \/ P_C) /\ (P_B1 \/ (not P_B2) \/ P_C)
[wp] [Alt-Ergo] Goal typed_f_ensures_c3 : Valid
[wp:cnf]
@@ -301,12 +299,12 @@
[wp:cnf] CNF=P_C /\ ((not P_B) \/ P_C) /\ ((not P_A) \/ (not P_B) \/ P_C)
[wp] [Alt-Ergo] Goal typed_f_ensures_e2 : Valid
[wp] Proved goals: 43 / 43
- Qed: 11
- Alt-Ergo: 32
+ Qed: 12
+ Alt-Ergo: 31
[wp] Report in: 'tests/wp_acsl/oracle_qualif/cnf.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/cnf.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-f 11 32 (336..384) 43 100%
+f 12 31 (336..384) 43 100%
-------------------------------------------------------------
[wp] Logging keys: success-only,shell,cnf.
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
index 5a458b3a95b..6a9e199c6af 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
@@ -175,7 +175,7 @@ Prove: (i + L_f(i)) != b.
------------------------------------------------------------
Goal Post-condition 'ko4' in 'forall':
-Prove: P_P(i) \/ (forall i_1 : Z. L_f(i_1) != i).
+Prove: (L_f(i) != i_1) \/ P_P(i_1).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 73e10138773..01958b282d4 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -119,7 +119,7 @@ hash 6 1 (12..24) 7 100%
size 2 - 2 100%
init 8 5 (72..96) 13 100%
add 24 15 (384..432) 39 100%
-mem_binding 18 8 (192..240) 26 100%
+mem_binding 18 8 (336..384) 26 100%
-------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function add
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 466000394e6..099a8b0731a 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
@@ -343,37 +343,34 @@ Prove: true.
Goal Loop assigns 'lack,Zone' (2/3):
Effect at line 139
Let a = global(G_t2_50).
-Let a_1 = shift_A20_sint32(a, i).
+Let a_1 = shift_A20_sint32(a, i_2).
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone' *)
Have: forall a_2 : addr.
- ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_2)))))) ->
+ ((forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_8), i_7) != a_2)))))) ->
(Mint_0[a_2] = Mint_1[a_2])).
(* Invariant 'Partial' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) ->
- (Mint_1[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_8), i_7)] = v))))).
(* Invariant 'Range' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_3)] = v))).
+ [shift_sint32(a_1, i_7)] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -630,31 +627,30 @@ Effect at line 157
Let a = global(G_t2_50).
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).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* 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)))) ->
+ ((forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_7), i_6) != a_2)))) ->
(Mint_0[a_2] = Mint_1[a_2])).
(* Invariant 'Partial' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) ->
- (Mint_1[shift_sint32(shift_A20_sint32(a, i_6), i_5)] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_7), i_6)] = 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) ->
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_5)] = v))).
+ [shift_sint32(a_1, i_6)] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1023,78 +1019,74 @@ Prove: true.
Goal Loop assigns 'lack,Zone_i' (2/3):
Effect at line 51
Assume {
- Type: is_uint32(i).
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
+ (t2_2[i_2][i_7] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
Goal Loop assigns 'lack,Zone_i' (3/3):
Effect at line 58
Assume {
- Type: is_uint32(i).
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
+ (t2_2[i_2][i_7] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -1106,43 +1098,40 @@ Prove: true.
Goal Loop assigns 'lack,Zone_j' (2/3):
Effect at line 58
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
+ Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 < j) -> (t2_2[i_2][i_7] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -1505,70 +1494,68 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 80
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
- (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
+ (t2_2[i_2][i_6] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
Goal Loop assigns 'tactic,Zone_i' (3/3):
Effect at line 87
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
- (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
+ (t2_2[i_2][i_6] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1580,38 +1567,37 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_j' (2/3):
Effect at line 87
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < j) -> (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_2[i_2][i_6] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1914,19 +1900,18 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 111
Assume {
- Have: 0 <= i.
- Have: i <= 9.
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).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_1[i_6][i_5] = t2_0[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_1[i_7][i_6] = t2_0[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
- P_MemSet20(t2_0[i_5], 20, v_1))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_2) ->
+ P_MemSet20(t2_0[i_6], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
@@ -1934,8 +1919,8 @@ Assume {
(* Invariant 'Partial_j' *)
Have: P_MemSet20(v, 20, v_1).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
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 d91b34a47a4..620a41fc301 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
@@ -343,37 +343,34 @@ Prove: true.
Goal Loop assigns 'lack,Zone' (2/3):
Effect at line 139
Let a = global(G_t2_50).
-Let a_1 = shift_A20_sint32(a, i).
+Let a_1 = shift_A20_sint32(a, i_2).
Assume {
- Type: is_uint32(i) /\ is_sint32(v).
+ Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone' *)
Have: forall a_2 : addr.
- ((forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (shift_sint32(shift_A20_sint32(a, i_4), i_3) != a_2)))))) ->
+ ((forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (shift_sint32(shift_A20_sint32(a, i_8), i_7) != a_2)))))) ->
(Mint_0[a_2] = Mint_1[a_2])).
(* Invariant 'Partial' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) ->
- (Mint_1[shift_sint32(shift_A20_sint32(a, i_4), i_3)] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_8), i_7)] = v))))).
(* Invariant 'Range' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Call 'init' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_3)] = v))).
+ [shift_sint32(a_1, i_7)] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -630,31 +627,30 @@ Effect at line 157
Let a = global(G_t2_50).
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).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* 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)))) ->
+ ((forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
+ (shift_sint32(shift_A20_sint32(a, i_7), i_6) != a_2)))) ->
(Mint_0[a_2] = Mint_1[a_2])).
(* Invariant 'Partial' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) ->
- (Mint_1[shift_sint32(shift_A20_sint32(a, i_6), i_5)] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) ->
+ (Mint_1[shift_sint32(shift_A20_sint32(a, i_7), i_6)] = 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) ->
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
- [shift_sint32(a_1, i_5)] = v))).
+ [shift_sint32(a_1, i_6)] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1023,78 +1019,74 @@ Prove: true.
Goal Loop assigns 'lack,Zone_i' (2/3):
Effect at line 51
Assume {
- Type: is_uint32(i).
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
+ (t2_2[i_2][i_7] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
Goal Loop assigns 'lack,Zone_i' (3/3):
Effect at line 58
Assume {
- Type: is_uint32(i).
+ Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 19) ->
+ (t2_2[i_2][i_7] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -1106,43 +1098,40 @@ Prove: true.
Goal Loop assigns 'lack,Zone_j' (2/3):
Effect at line 58
Assume {
- Type: is_uint32(i) /\ is_uint32(j).
+ Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i_6) /\ (0 <= i) /\
+ (0 <= i_1) /\ (i_3 <= 9) /\ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19) /\
+ (i_6 <= 19) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_0[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_1[i_8][i_7] = v))))).
(* Invariant 'Range_i' *)
- Have: (0 <= i) /\ (i <= 10).
+ Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
- Have: i <= 9.
+ Have: i_2 <= 9.
(* Loop assigns 'lack,Zone_j' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((0 <= i_7) -> ((i_8 <= 9) ->
+ ((i_7 <= 19) ->
+ (((i_8 < 0) \/ (i_7 < 0) \/ (10 <= i_8) \/ (20 <= i_7)) ->
+ (t2_2[i_8][i_7] = t2_1[i_8][i_7])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ Have: forall i_8,i_7 : Z. ((0 <= i_8) -> ((i_8 < i_2) -> ((0 <= i_7) ->
+ ((i_7 <= 19) -> (t2_2[i_8][i_7] = t2_1[i_8][i_7]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ Have: forall i_7 : Z. ((0 <= i_7) -> ((i_7 < j) -> (t2_2[i_2][i_7] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: exists i_8,i_7 : Z. (i_8 <= i) /\ (i_7 <= i_1) /\ (0 <= i_8) /\
+ (i <= i_8) /\ (0 <= i_7) /\ (i_1 <= i_7) /\ (i_8 <= 9) /\ (i_7 <= 19).
------------------------------------------------------------
@@ -1505,70 +1494,68 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 80
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
- (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
+ (t2_2[i_2][i_6] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
Goal Loop assigns 'tactic,Zone_i' (3/3):
Effect at line 87
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 19) ->
- (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 19) ->
+ (t2_2[i_2][i_6] = v))).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1580,38 +1567,37 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_j' (2/3):
Effect at line 87
Assume {
- Have: 0 <= i.
- Have: i <= 9.
Type: is_uint32(i_2) /\ is_uint32(j).
(* Goal *)
- When: (0 <= i_3) /\ (0 <= i_4) /\ (i_3 <= 9) /\ (i_4 <= 19).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_0[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_0[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_1[i_6][i_5] = v))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_1[i_7][i_6] = v))))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
Have: i_2 <= 9.
(* Loop assigns 'tactic,Zone_j' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_2[i_6][i_5] = t2_1[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_2[i_7][i_6] = t2_1[i_7][i_6])))))).
(* Invariant 'Previous_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((i_6 < i_2) -> ((0 <= i_5) ->
- ((i_5 <= 19) -> (t2_2[i_6][i_5] = t2_1[i_6][i_5]))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((i_7 < i_2) -> ((0 <= i_6) ->
+ ((i_6 <= 19) -> (t2_2[i_7][i_6] = t2_1[i_7][i_6]))))).
(* Invariant 'Partial_j' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < j) -> (t2_2[i_2][i_5] = v))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < j) -> (t2_2[i_2][i_6] = v))).
(* Invariant 'Range_j' *)
Have: (0 <= j) /\ (j <= 20).
(* Then *)
Have: j <= 19.
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
@@ -1914,19 +1900,18 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 111
Assume {
- Have: 0 <= i.
- Have: i <= 9.
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).
+ When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
+ (i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
(* Loop assigns 'tactic,Zone_i' *)
- Have: forall i_6,i_5 : Z. ((0 <= i_6) -> ((0 <= i_5) -> ((i_6 <= 9) ->
- ((i_5 <= 19) -> (((i_6 < 0) \/ (10 <= i_6)) ->
- (t2_1[i_6][i_5] = t2_0[i_6][i_5])))))).
+ Have: forall i_7,i_6 : Z. ((0 <= i_7) -> ((0 <= i_6) -> ((i_7 <= 9) ->
+ ((i_6 <= 19) -> (((i_7 < 0) \/ (10 <= i_7)) ->
+ (t2_1[i_7][i_6] = t2_0[i_7][i_6])))))).
(* Invariant 'Partial_i' *)
- Have: forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
- P_MemSet20(t2_0[i_5], 20, v_1))).
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 < i_2) ->
+ P_MemSet20(t2_0[i_6], 20, v_1))).
(* Invariant 'Range_i' *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Then *)
@@ -1934,8 +1919,8 @@ Assume {
(* Invariant 'Partial_j' *)
Have: P_MemSet20(v, 20, v_1).
}
-Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (0 <= i_6) /\
- (i <= i_6) /\ (i_1 <= i_5) /\ (i_6 <= 9).
+Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
+ (i <= i_7) /\ (i_1 <= i_6) /\ (i_7 <= 9).
------------------------------------------------------------
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 ef5a6f0f00a..feb4222c312 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
@@ -43,7 +43,7 @@
[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_v2 3 - (20..32) 8 100%
init_t2_v3 4 - (20..32) 7 100%
init_t2_bis_v2 4 - (28..40) 8 100%
-------------------------------------------------------------
--
GitLab