From 57c8e5094dad03537791f512b96130a7ccbc247e Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 21 Feb 2019 13:55:54 +0100
Subject: [PATCH] [WP/test] adding a test initializing multidimentianal arrays
---
.../wp_typed/oracle/user_init.0.res.oracle | 777 ++++++++++++++++++
.../wp_typed/oracle/user_init.1.res.oracle | 777 ++++++++++++++++++
.../oracle_qualif/user_init.0.report.json | 217 ++++-
.../oracle_qualif/user_init.i.0.report.json | 217 ++++-
.../oracle_qualif/user_init.res.oracle | 59 +-
src/plugins/wp/tests/wp_typed/user_init.i | 60 ++
6 files changed, 2095 insertions(+), 12 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 6002f927642..7b2ee670197 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function init
@@ -116,3 +118,778 @@ Effect at line 12
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 16) in 'init_t1':
+Assume {
+ Type: is_uint32(i_1).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 9).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_1) /\ (i_1 <= 10).
+ (* Else *)
+ Have: 10 <= i_1.
+}
+Prove: t1_0[i] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: t1_0[i <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (1/2):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (2/2):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 30) in 'init_t2':
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: m[j <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (m[i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'j' (file tests/wp_typed/user_init.i, line 50):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 53):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (2/3):
+Effect at line 41
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (3/3):
+Effect at line 47
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (2/3):
+Effect at line 47
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (3/3):
+Effect at line 48
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: j <= 20.
+}
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
+ (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (1/2):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (2/2):
+Effect at line 41
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 57) in 'init_t2_bis':
+Assume {
+ Type: is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 59) in 'init_t2_bis':
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Exit Effects *)
+ Have: (forall i_1 : Z. ((i_1 != i) -> (t2_2[i_1] = t2_1[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (20 <= i_1)) -> (t2_2[i][i_1] = t2_1[i][i_1]))))).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Let m = t2_0[i].
+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 ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+ (* Call Effects *)
+ Have: (forall i_3 : Z. ((i_3 != i) -> (t2_2[i_3] = t2_0[i_3]))) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (20 <= i_3)) -> (t2_2[i][i_3] = m[i_3]))))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (m[i_1] = v))).
+ (* Call Effects *)
+ Have: (forall i_1 : Z. ((i_1 != i) -> (t2_1[i_1] = t2_2[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (20 <= i_1)) -> (t2_1[i][i_1] = m[i_1]))))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (2/3):
+Effect at line 68
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+ (* Call Effects *)
+ Have: (forall i_3 : Z. ((i_3 != i) -> (t2_1[i_3] = t2_2[i_3]))) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (20 <= i_3)) -> (t2_1[i][i_3] = m[i_3]))))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (3/3):
+Call Effect at line 69
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (m[i_2] = v))).
+ (* Call Effects *)
+ Have: (forall i_2 : Z. ((i_2 != i) -> (t2_1[i_2] = t2_2[i_2]))) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (20 <= i_2)) -> (t2_1[i][i_2] = m[i_2]))))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/3):
+Effect at line 68
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/3):
+Effect at line 68
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (3/3):
+Call Effect at line 69
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Exit Effects *)
+ Have: (forall i_2 : Z. ((i_2 != i) -> (t2_2[i_2] = t2_1[i_2]))) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (20 <= i_2)) -> (t2_2[i][i_2] = t2_1[i][i_2]))))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/2):
+Effect at line 68
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/2):
+Effect at line 68
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 1) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 2) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
+:
+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 69788521bcf..fa09d252394 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function init
@@ -116,3 +118,778 @@ Effect at line 12
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 16) in 'init_t1':
+Assume {
+ Type: is_uint32(i_1).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 9).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i_1) /\ (i_1 <= 10).
+ (* Else *)
+ Have: 10 <= i_1.
+}
+Prove: t1_0[i] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
+ (* Invariant 'Partial' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (t1_0[i_2] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: t1_0[i <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 23):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Assume {
+ Type: is_uint32(i).
+ (* Invariant 'Partial' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) -> (t1_0[i_1] = v))).
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file tests/wp_typed/user_init.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (1/2):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 18) in 'init_t1' (2/2):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 30) in 'init_t2':
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 39):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Assume {
+ Type: is_uint32(i).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (t2_2[i][i_1] = v))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_2[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_2[i_3][i_2])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = t2_2[i_3][i_2]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < j) -> (m[i_2] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: m[j <- v][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Let m = t2_0[i].
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (m[i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: t2_0[i <- m[j <- v]][i_1][i_2] = t2_1[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Previous_i' (file tests/wp_typed/user_init.i, line 45):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: to_uint32(1 + j) <= 20.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 43):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'j' (file tests/wp_typed/user_init.i, line 50):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 53):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (2/3):
+Effect at line 41
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 37) (3/3):
+Effect at line 47
+Assume {
+ Type: is_uint32(i).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (2/3):
+Effect at line 47
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_2[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_1[i_4][i_3]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < j) -> (t2_2[i][i_3] = v))).
+ (* Invariant 'Range_j' *)
+ Have: (0 <= j) /\ (j <= 20).
+ (* Then *)
+ Have: j <= 19.
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 42) (3/3):
+Effect at line 48
+Assume {
+ Type: is_uint32(i) /\ is_uint32(j).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_2[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Previous_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_2[i_2][i_1] = t2_1[i_2][i_1]))))).
+ (* Invariant 'Partial_j' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) -> (t2_2[i][i_1] = v))).
+ (* Invariant 'Range_j' *)
+ Have: j <= 20.
+}
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_1) /\
+ (j <= i_1) /\ (0 <= i_2) /\ (i <= i_2) /\ (i_2 <= 9) /\ (i_1 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (1/2):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 32) in 'init_t2' (2/2):
+Effect at line 41
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function init_t2_bis
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_typed/user_init.i, line 57) in 'init_t2_bis':
+Assume {
+ Type: is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_1[i_3][i_2] = t2_0[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) -> (t2_0[i_3][i_2] = v))))).
+}
+Prove: t2_0[i][i_1] = v.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_typed/user_init.i, line 59) in 'init_t2_bis':
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Exit Effects *)
+ Have: (forall i_1 : Z. ((i_1 != i) -> (t2_2[i_1] = t2_1[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (20 <= i_1)) -> (t2_2[i][i_1] = t2_1[i][i_1]))))).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Let m = t2_0[i].
+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 ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_1[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+ (* Call Effects *)
+ Have: (forall i_3 : Z. ((i_3 != i) -> (t2_2[i_3] = t2_0[i_3]))) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (20 <= i_3)) -> (t2_2[i][i_3] = m[i_3]))))).
+}
+Prove: m[0] = t2_0[i_1][i_2].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 66):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Loop assigns ... *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (i_2 < 0) \/ (10 <= i_2) \/ (20 <= i_1)) ->
+ (t2_0[i_2][i_1] = t2_1[i_2][i_1])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_2,i_1 : Z. ((0 <= i_1) -> ((0 <= i_2) -> ((i_2 < i) ->
+ ((i_1 <= 19) -> (t2_1[i_2][i_1] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) -> (m[i_1] = v))).
+ (* Call Effects *)
+ Have: (forall i_1 : Z. ((i_1 != i) -> (t2_1[i_1] = t2_2[i_1]))) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
+ (((i_1 < 0) \/ (20 <= i_1)) -> (t2_1[i][i_1] = m[i_1]))))).
+}
+Prove: to_uint32(1 + i) <= 10.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 65):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'i' (file tests/wp_typed/user_init.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (2/3):
+Effect at line 68
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 <= 9) /\ (i_2 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (i_4 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
+ (t2_0[i_4][i_3] = t2_1[i_4][i_3])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 < i) ->
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: (0 <= i) /\ (i <= 10).
+ (* Then *)
+ Have: i <= 9.
+ (* Call 'init' *)
+ Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
+ (* Call Effects *)
+ Have: (forall i_3 : Z. ((i_3 != i) -> (t2_1[i_3] = t2_2[i_3]))) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) ->
+ (((i_3 < 0) \/ (20 <= i_3)) -> (t2_1[i][i_3] = m[i_3]))))).
+}
+Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) -> false))))) \/
+ (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
+ ((i_3 <= 19) ->
+ (exists i_6,i_5 : Z. (0 <= i_5) /\ (i_3 <= i_5) /\ (0 <= i_6) /\
+ (i_4 <= i_6) /\ (i_5 <= i_3) /\ (i_6 <= i_4) /\ (i_6 <= 9) /\
+ (i_5 <= 19))))))).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_typed/user_init.i, line 64) (3/3):
+Call Effect at line 69
+Let m = t2_2[i].
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Call 'init' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) -> (m[i_2] = v))).
+ (* Call Effects *)
+ Have: (forall i_2 : Z. ((i_2 != i) -> (t2_1[i_2] = t2_2[i_2]))) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (20 <= i_2)) -> (t2_1[i][i_2] = m[i_2]))))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/3):
+Effect at line 68
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/3):
+Effect at line 68
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (3/3):
+Call Effect at line 69
+Assume {
+ Type: is_uint32(i) /\ is_sint32(v).
+ (* Goal *)
+ When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
+ (* Loop assigns ... *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 <= 9) ->
+ ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (i_3 < 0) \/ (10 <= i_3) \/ (20 <= i_2)) ->
+ (t2_0[i_3][i_2] = t2_1[i_3][i_2])))))).
+ (* Invariant 'Partial_i' *)
+ Have: forall i_3,i_2 : Z. ((0 <= i_2) -> ((0 <= i_3) -> ((i_3 < i) ->
+ ((i_2 <= 19) -> (t2_1[i_3][i_2] = v))))).
+ (* Invariant 'Range_i' *)
+ Have: i <= 10.
+ (* Exit Effects *)
+ Have: (forall i_2 : Z. ((i_2 != i) -> (t2_2[i_2] = t2_1[i_2]))) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 19) ->
+ (((i_2 < 0) \/ (20 <= i_2)) -> (t2_2[i][i_2] = t2_1[i][i_2]))))).
+}
+Prove: exists i_3,i_2 : Z. (i_3 <= i) /\ (i_2 <= i_1) /\ (0 <= i_2) /\
+ (i_1 <= i_2) /\ (0 <= i_3) /\ (i <= i_3) /\ (i_3 <= 9) /\ (i_2 <= 19).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (1/2):
+Effect at line 68
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_typed/user_init.i, line 58) in 'init_t2_bis' (2/2):
+Effect at line 68
+Assume {
+ Have: 0 <= i_2.
+ Have: 0 <= i_3.
+ Have: i_2 <= 9.
+ Have: i_3 <= 19.
+ Have: 0 <= i.
+ Have: 0 <= i_1.
+ Have: i <= 9.
+ Have: i_1 <= 19.
+ (* Loop assigns ... *)
+ Have: forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (((i_4 < 0) \/ (i_5 < 0) \/ (10 <= i_5) \/ (20 <= i_4)) ->
+ (t2_0[i_5][i_4] = t2_1[i_5][i_4])))))).
+}
+Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
+ (i_1 <= i_4) /\ (0 <= i_5) /\ (i <= i_5) /\ (i_5 <= 9) /\ (i_4 <= 19).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 1) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_init.i, line 2) in 'init'' in 'init_t2_bis' at call 'init' (file tests/wp_typed/user_init.i, line 69)
+:
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
index ab542867843..7bfbab0fa17 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
@@ -1,6 +1,8 @@
-{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 19 },
- "qed": { "total": 4, "valid": 4 },
- "wp:main": { "total": 8, "valid": 8, "rank": 19 } },
+{ "wp:global": { "alt-ergo": { "total": 27, "valid": 16, "unknown": 11,
+ "rank": 19 },
+ "qed": { "total": 27, "valid": 27 },
+ "wp:main": { "total": 54, "valid": 43, "unknown": 11,
+ "rank": 19 } },
"wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo":
{ "total": 1,
"valid": 1,
@@ -47,4 +49,211 @@
"valid": 4 },
"wp:main": { "total": 8,
"valid": 8,
- "rank": 19 } } } } }
+ "rank": 19 } } },
+ "init_t1": { "init_t1_loop_invariant_Partial": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 4 } },
+ "init_t1_loop_invariant_Range": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 2 } },
+ "init_t1_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "init_t1_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_t1_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 4 },
+ "qed": { "total": 5,
+ "valid": 5 },
+ "wp:main": { "total": 8,
+ "valid": 8,
+ "rank": 4 } } },
+ "init_t2": { "init_t2_assert_i": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_assert_j": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_loop_invariant_Previous_i":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 5 } },
+ "init_t2_loop_invariant_Partial_j":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 8 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 8 } },
+ "init_t2_loop_invariant_Range_j": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 3 } },
+ "init_t2_loop_invariant_Partial_i":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 11 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 11 } },
+ "init_t2_loop_invariant_Range_i": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 2 } },
+ "init_t2_assigns": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } },
+ "init_t2_loop_assigns_2": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_loop_assigns": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "wp:section": { "alt-ergo": { "total": 11,
+ "valid": 6,
+ "unknown": 5,
+ "rank": 11 },
+ "qed": { "total": 10,
+ "valid": 10 },
+ "wp:main": { "total": 21,
+ "valid": 16,
+ "unknown": 5,
+ "rank": 11 } } },
+ "init_t2_bis": { "init_requires_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_requires": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_bis_assert_i": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_t2_bis_loop_invariant_Partial_i":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 10 } },
+ "init_t2_bis_loop_invariant_Range_i":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 3 } },
+ "init_t2_bis_assigns": { "alt-ergo":
+ { "total": 3,
+ "unknown": 3 },
+ "qed":
+ { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 5,
+ "valid": 2,
+ "unknown": 3 } },
+ "init_t2_bis_loop_assigns": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_bis_exits": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "init_t2_bis_ensures": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 9,
+ "valid": 3,
+ "unknown": 6,
+ "rank": 10 },
+ "qed": { "total": 8,
+ "valid": 8 },
+ "wp:main": { "total": 17,
+ "valid": 11,
+ "unknown": 6,
+ "rank": 10 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.i.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.i.0.report.json
index 1651d4db136..0b74bede002 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.i.0.report.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.i.0.report.json
@@ -1,6 +1,8 @@
-{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 19 },
- "qed": { "total": 4, "valid": 4 },
- "wp:main": { "total": 8, "valid": 8, "rank": 19 } },
+{ "wp:global": { "alt-ergo": { "total": 27, "valid": 16, "unknown": 11,
+ "rank": 19 },
+ "qed": { "total": 27, "valid": 27 },
+ "wp:main": { "total": 54, "valid": 43, "unknown": 11,
+ "rank": 19 } },
"wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo":
{ "total": 1,
"valid": 1,
@@ -47,4 +49,211 @@
"valid": 4 },
"wp:main": { "total": 8,
"valid": 8,
- "rank": 19 } } } } }
+ "rank": 19 } } },
+ "init_t1": { "init_t1_loop_invariant_Partial": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 4 } },
+ "init_t1_loop_invariant_Range": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 2 } },
+ "init_t1_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "init_t1_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_t1_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 4 },
+ "qed": { "total": 5,
+ "valid": 5 },
+ "wp:main": { "total": 8,
+ "valid": 8,
+ "rank": 4 } } },
+ "init_t2": { "init_t2_assert_i": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_assert_j": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_loop_invariant_Previous_i":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 5 } },
+ "init_t2_loop_invariant_Partial_j":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 8 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 8 } },
+ "init_t2_loop_invariant_Range_j": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 3 } },
+ "init_t2_loop_invariant_Partial_i":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 11 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 11 } },
+ "init_t2_loop_invariant_Range_i": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 2 } },
+ "init_t2_assigns": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } },
+ "init_t2_loop_assigns_2": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_loop_assigns": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "wp:section": { "alt-ergo": { "total": 11,
+ "valid": 6,
+ "unknown": 5,
+ "rank": 11 },
+ "qed": { "total": 10,
+ "valid": 10 },
+ "wp:main": { "total": 21,
+ "valid": 16,
+ "unknown": 5,
+ "rank": 11 } } },
+ "init_t2_bis": { "init_requires_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_requires": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_t2_bis_assert_i": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "init_t2_bis_loop_invariant_Partial_i":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 10 } },
+ "init_t2_bis_loop_invariant_Range_i":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2,
+ "rank": 3 } },
+ "init_t2_bis_assigns": { "alt-ergo":
+ { "total": 3,
+ "unknown": 3 },
+ "qed":
+ { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 5,
+ "valid": 2,
+ "unknown": 3 } },
+ "init_t2_bis_loop_assigns": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 3,
+ "valid": 1,
+ "unknown": 2 } },
+ "init_t2_bis_exits": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "init_t2_bis_ensures": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 9,
+ "valid": 3,
+ "unknown": 6,
+ "rank": 10 },
+ "qed": { "total": 8,
+ "valid": 8 },
+ "wp:main": { "total": 17,
+ "valid": 11,
+ "unknown": 6,
+ "rank": 10 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
index 6f23e12122e..4166c7752ea 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle
@@ -2,8 +2,10 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
+[wp] [CFG] Goal init_t2_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] 8 goals scheduled
+[wp] 54 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
@@ -12,12 +14,61 @@
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns : Valid
-[wp] Proved goals: 8 / 8
- Qed: 4
- Alt-Ergo: 4
+[wp] [Alt-Ergo] Goal typed_init_t1_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Partial_preserved : Valid
+[wp] [Qed] Goal typed_init_t1_loop_invariant_Partial_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t1_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_t1_loop_invariant_Range_established : Valid
+[wp] [Qed] Goal typed_init_t1_loop_assigns : Valid
+[wp] [Qed] Goal typed_init_t1_assigns_part1 : Valid
+[wp] [Qed] Goal typed_init_t1_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Partial_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_loop_invariant_Partial_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Range_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_loop_invariant_Range_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Partial_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_loop_invariant_Partial_j_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Previous_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_loop_invariant_Previous_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_invariant_Range_j_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_loop_invariant_Range_j_established : Valid
+[wp] [Qed] Goal typed_init_t2_assert_j : Valid
+[wp] [Qed] Goal typed_init_t2_assert_i : Valid
+[wp] [Qed] Goal typed_init_t2_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_loop_assigns_2_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_2_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_loop_assigns_2_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_exits : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_invariant_Partial_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_loop_invariant_Partial_i_established : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_invariant_Range_i_preserved : Valid
+[wp] [Qed] Goal typed_init_t2_bis_loop_invariant_Range_i_established : Valid
+[wp] [Qed] Goal typed_init_t2_bis_assert_i : Valid
+[wp] [Qed] Goal typed_init_t2_bis_loop_assigns_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_assigns_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_loop_assigns_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_assigns_exit_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_exit_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_exit_part3 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_assigns_normal_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_init_t2_bis_assigns_normal_part2 : Unsuccess
+[wp] [Qed] Goal typed_init_t2_bis_call_init_requires : Valid
+[wp] [Qed] Goal typed_init_t2_bis_call_init_requires_2 : Valid
+[wp] Proved goals: 43 / 54
+ Qed: 27
+ Alt-Ergo: 16 (unsuccess: 11)
[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json'
[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 4 4 (80..104) 8 100%
+init_t1 5 3 (12..24) 8 100%
+init_t2 10 6 (40..52) 21 76.2%
+init_t2_bis 8 3 (36..48) 17 64.7%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index a7ab761501f..416a94e97e0 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -11,3 +11,63 @@ void init( int * a , int n , int v )
*/
for (int i = 0 ; i < n ; i++) a[i] = v ;
}
+//-------------------------
+int t1[10];
+/*@ ensures \forall integer k; 0 <= k < 10 ==> t1[k] == v ;
+ @ exits \false;
+ @ assigns t1[0..9] ;
+*/
+void init_t1(int v) {
+ unsigned i;
+ /*@ loop invariant Range: 0 <= i <= 10 ;
+ @ loop invariant Partial: \forall integer k ; 0 <= k < i ==> t1[k] ≡ v ;
+ @ loop assigns i,t1[0..9] ;
+ */
+ for (i = 0 ; i < 10 ; i++) t1[i] = v ;
+}
+//-------------------------
+int t2[10][20];
+/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+ @ exits \false;
+ @ assigns t2[0..9][0..19];
+ */
+void init_t2(int v) {
+
+ unsigned i,j;
+ /*@ loop assigns i, j, t2[0..9][0..19];
+ @ loop invariant Range_i: 0 <= i <= 10 ;
+ @ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ */
+ for(i = 0; i <= 9; i++) {
+ /*@ loop assigns j, t2[0..9][0..19];
+ @ loop invariant Range_j: 0 <= j <= 20 ;
+ @ loop invariant Partial_j: \forall integer l; 0 <= l < j ==> t2[i][l] == v;
+ @ loop invariant Previous_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == \at(t2[k][l], LoopEntry);
+ */
+ for(j = 0; j <= 19; j++) {
+ t2[i][j] = v;
+ }
+ //@ assert j: j==20;
+ ;
+ }
+ //@ assert i: i==10;
+ ;
+}
+//-------------------------
+/*@ ensures \forall integer k, l; 0 <= k < 10 && 0 <= l < 20 ==> t2[k][l] == v;
+ @ assigns t2[0..9][0..19];
+ @ exits \false;
+ */
+void init_t2_bis(int v) {
+
+ unsigned i;
+ /*@ loop assigns i, t2[0..9][0..19];
+ @ loop invariant Range_i: 0 <= i <= 10 ;
+ @ loop invariant Partial_i: \forall integer k,l; 0 <= k < i && 0 <= l < 20 ==> t2[k][l] == v;
+ */
+ for(i = 0; i <= 9; i++) {
+ init(&t2[i][0], 20, v);
+ }
+ //@ assert i: i==10;
+ ;
+}
--
GitLab