From 90676872836e95fa2816910ca92f640de3bdbb32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 12:27:53 +0200
Subject: [PATCH] [wp] renamed is-array predicates
---
src/plugins/wp/Cvalues.ml | 13 +-
.../wp_acsl/oracle/assigns_range.res.oracle | 10 +-
.../wp_acsl/oracle/chunk_typing.res.oracle | 2 +-
.../wp/tests/wp_acsl/oracle/equal.res.oracle | 10 +-
.../wp_acsl/oracle/funvar_inv.0.res.oracle | 12 +-
.../wp_acsl/oracle/init_label.res.oracle | 4 +-
.../wp_acsl/oracle/init_value.0.res.oracle | 174 ++++++++----------
.../wp_acsl/oracle/init_value.1.res.oracle | 79 ++++----
.../wp/tests/wp_acsl/oracle/logic.res.oracle | 8 +-
.../wp/tests/wp_acsl/oracle/record.res.oracle | 2 +-
.../wp/tests/wp_bts/oracle/bts788.res.oracle | 4 +-
.../tests/wp_hoare/oracle/logicarr.res.oracle | 12 +-
.../oracle/reference_and_struct.res.oracle | 4 +-
.../oracle/reference_array.res.oracle | 20 +-
.../wp_plugin/oracle/init_const.res.oracle | 4 +-
.../wp_plugin/oracle/injector.res.oracle | 8 +-
.../wp_plugin/oracle/overarray.res.oracle | 8 +-
.../oracle/array_initialized.0.res.oracle | 4 +-
.../tests/wp_typed/oracle/frame.0.res.oracle | 4 +-
.../tests/wp_typed/oracle/frame.1.res.oracle | 4 +-
.../tests/wp_typed/oracle/mvar.0.res.oracle | 2 +-
.../tests/wp_typed/oracle/mvar.1.res.oracle | 2 +-
.../oracle/struct_array_type.res.oracle | 11 +-
.../wp_typed/oracle/unit_matrix.0.res.oracle | 4 +-
.../wp_typed/oracle/unit_matrix.1.res.oracle | 4 +-
.../wp_typed/oracle/user_collect.0.res.oracle | 42 ++---
.../wp_typed/oracle/user_collect.1.res.oracle | 42 ++---
.../wp_typed/oracle/user_init.0.res.oracle | 60 +++---
.../wp_typed/oracle/user_init.1.res.oracle | 60 +++---
.../script/init_t2_v3_loop_assigns_part2.json | 4 +-
.../script/init_t2_v3_loop_assigns_part3.json | 4 +-
31 files changed, 294 insertions(+), 327 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 216b2cedafe..a56d4459849 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -126,17 +126,14 @@ struct
let array_name te ds =
let dim = List.length ds in
+ let pp_dim fmt d = if d > 1 then Format.fprintf fmt "_d%d" d in
match te with
| C_int i ->
- Format.asprintf "%sArray%d_%a" C.prefix dim model_int i
- | C_float _ ->
- Format.asprintf "%sArray%d_float" C.prefix dim
- | C_pointer _ ->
- Format.asprintf "%sArray%d_pointer" C.prefix dim
+ Format.asprintf "%sArray%a_%a" C.prefix pp_dim dim model_int i
| C_comp c ->
- Format.asprintf "%sArray%d%s" C.prefix dim (Lang.comp_id c)
- | C_array _ ->
- Wp_parameters.fatal "Unflatten array (%s %a)" C.prefix Ctypes.pretty te
+ Format.asprintf "%sArray%a_%s" C.prefix pp_dim dim (Lang.comp_id c)
+ | C_float _ | C_pointer _ | C_array _ ->
+ assert false
let rec is_obj obj t =
match obj with
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
index 47e610fd265..221a2fec8a8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
@@ -92,7 +92,7 @@ Goal Instance of 'Pre-condition (file tests/wp_acsl/assigns_range.i, line 23) in
Assume {
Type: is_sint32(i) /\ is_sint32(j).
(* Heap *)
- Type: IsArray1_sint32(t2_0) /\ IsArray1_sint32(t3_0).
+ Type: IsArray_sint32(t2_0) /\ IsArray_sint32(t3_0).
(* Pre-condition *)
Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Call 'assigns_t1_an_element' *)
@@ -153,7 +153,7 @@ Call Effect at line 57
Assume {
Type: is_sint32(i).
(* Heap *)
- Type: IsArray1_sint32(t2_0).
+ Type: IsArray_sint32(t2_0).
(* Goal *)
When: ((-2) <= i) /\ (i <= 19).
(* Pre-condition *)
@@ -173,7 +173,7 @@ Call Effect at line 57
Assume {
Type: is_sint32(i).
(* Heap *)
- Type: IsArray1_sint32(t2_0).
+ Type: IsArray_sint32(t2_0).
(* Goal *)
When: ((-2) <= i) /\ (i <= 19).
(* Pre-condition *)
@@ -204,7 +204,7 @@ Call Effect at line 65
Assume {
Type: is_sint32(i) /\ is_sint32(j).
(* Heap *)
- Type: IsArray1_sint32(t4_0).
+ Type: IsArray_sint32(t4_0).
(* Goal *)
When: 0 <= j.
(* Pre-condition *)
@@ -222,7 +222,7 @@ Call Effect at line 65
Assume {
Type: is_sint32(i) /\ is_sint32(j).
(* Heap *)
- Type: IsArray1_sint32(t4_0).
+ Type: IsArray_sint32(t4_0).
(* Goal *)
When: 0 <= j.
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index e9965d8c184..e139ffdc57f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -31,7 +31,7 @@ Let a_20 = a_9[shift_sint32(i32_0, i)].
Let a_21 = a_11[shift_uint32(u32_0, i)].
Let a_22 = a_13[shift_sint64(i64_0, i)].
Assume {
- Type: IsArray1_sint8(x) /\ is_sint16_chunk(Mint_1) /\
+ Type: IsArray_sint8(x) /\ is_sint16_chunk(Mint_1) /\
is_sint32_chunk(Mint_3) /\ is_sint64_chunk(Mint_5) /\
is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
index a543f1f54a2..202dde2b9d6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
@@ -10,7 +10,7 @@ Goal Post-condition (file tests/wp_acsl/equal.i, line 22) in 'simple_array':
Let x = t0_0[0].
Let x_1 = t0_0[1].
Assume {
- Type: IsArray1_sint32(t0_0) /\ IsArray1_sint32(t1_0) /\ is_sint32(x) /\
+ Type: IsArray_sint32(t0_0) /\ IsArray_sint32(t1_0) /\ is_sint32(x) /\
is_sint32(x_1).
}
Prove: EqArray1_int(2, t0_0, t1_0[0 <- x][1 <- x_1]).
@@ -32,8 +32,8 @@ Goal Post-condition (file tests/wp_acsl/equal.i, line 28) in 'with_array_struct'
Let a = st0_0.F2_St_tab.
Let a_1 = st1_0.F2_St_tab.
Assume {
- Type: IsS2_St(st0_0) /\ IsS2_St(st1_0) /\ IsArray1_sint32(a) /\
- IsArray1_sint32(a_1).
+ Type: IsS2_St(st0_0) /\ IsS2_St(st1_0) /\ IsArray_sint32(a) /\
+ IsArray_sint32(a_1).
(* Goal *)
When: EqArray1_int(10, a, a_1).
}
@@ -52,8 +52,8 @@ Let a_3 = q1_0.F4_Q_qs.
Let a_4 = q0_0.F4_Q_qt.
Let a_5 = q1_0.F4_Q_qt.
Assume {
- Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray1_sint32(a_4) /\
- IsArray1_sint32(a_5) /\ IsS1_S(a_2) /\ IsS1_S(a_3).
+ Type: IsS4_Q(q0_0) /\ IsS4_Q(q1_0) /\ IsArray_sint32(a_4) /\
+ IsArray_sint32(a_5) /\ IsS1_S(a_2) /\ IsS1_S(a_3).
(* Heap *)
Type: (region(a_1.base) <= 0) /\ (region(a.base) <= 0).
(* Goal *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
index a6492896347..dcd51036376 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
@@ -26,7 +26,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x) /\ is_sint32(G[1]).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
If i <= 3
Then { (* Else *) Have: G[i] = 0. }
}
@@ -42,7 +42,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
(* Goal *)
When: (x != 0) /\ (G[1] = 0).
If i <= 3
@@ -68,7 +68,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x) /\ is_sint32(G[1]).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
If i <= 3
Then { (* Else *) Have: G[i] = 0. }
}
@@ -84,7 +84,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
(* Goal *)
When: (x != 0) /\ (G[1] = 0).
If i <= 3
@@ -110,7 +110,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x) /\ is_sint32(G[1]).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
If i <= 3
Then { (* Else *) Have: G[i] = 0. }
}
@@ -126,7 +126,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(G).
+ Type: IsArray_sint32(G).
(* Goal *)
When: (x != 0) /\ (G[1] = 0).
If i <= 3
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index d6d7a763dab..af8d7fd203c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -10,7 +10,7 @@
Goal Post-condition 'KO' in 'extra':
Let x = A[2].
-Assume { Type: is_sint32(x). (* Heap *) Type: IsArray1_sint32(A). }
+Assume { Type: is_sint32(x). (* Heap *) Type: IsArray_sint32(A). }
Prove: x = 12.
------------------------------------------------------------
@@ -29,7 +29,7 @@ Prove: true.
Goal Post-condition 'OK' in 'job':
Let x = A[2].
Assume {
- Type: IsArray1_sint32(A) /\ IsArray1_sint32(A_1) /\ is_sint32(x).
+ Type: IsArray_sint32(A) /\ IsArray_sint32(A_1) /\ is_sint32(x).
(* Initializer *)
Init: A_1[0] = 10.
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
index c072c17ac8b..3c0bd768f4e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
@@ -14,7 +14,7 @@ Let x_3 = ta1_0[3].
Assume {
Type: is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
(* Initializer *)
@@ -34,7 +34,7 @@ Assume {
Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(ta1_0[3]) /\
is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
(* Initializer *)
@@ -55,7 +55,7 @@ Assume {
Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(x_1) /\
is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta1_0[i] = 0))).
(* Initializer *)
@@ -79,7 +79,7 @@ Let x_2 = ta2_0[4].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
(* Initializer *)
@@ -96,7 +96,7 @@ Let x = ta2_0[4].
Assume {
Type: is_sint32(ta2_0[0]) /\ is_sint32(ta2_0[1]) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
(* Initializer *)
@@ -113,7 +113,7 @@ Let x = ta2_0[1].
Assume {
Type: is_sint32(ta2_0[0]) /\ is_sint32(x) /\ is_sint32(ta2_0[4]).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
(* Initializer *)
Init: forall i : Z. ((0 <= i) -> ((i <= 1) -> (ta2_0[i] = 0))).
(* Initializer *)
@@ -137,8 +137,8 @@ Assume {
Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(ta2_0[4]) /\
is_sint32(x_2) /\ is_sint32(x_3).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
(* Initializer *)
Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
(* Initializer *)
@@ -176,8 +176,8 @@ Assume {
Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(ta2_0[4]) /\
is_sint32(x_2) /\ is_sint32(ta3_0[2]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
(* Initializer *)
Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
(* Initializer *)
@@ -215,8 +215,8 @@ Assume {
Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(ta2_0[4]) /\
is_sint32(ta3_0[0]) /\ is_sint32(x_2).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
(* Initializer *)
Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
(* Initializer *)
@@ -254,8 +254,8 @@ Assume {
Type: is_sint32(x_1) /\ is_sint32(x) /\ is_sint32(x_2) /\
is_sint32(ta3_0[0]) /\ is_sint32(ta3_0[2]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
(* Initializer *)
Init: forall i : Z. ((i <= 0) -> ((0 <= i) -> (ta3_0[i] = 0))).
(* Initializer *)
@@ -300,7 +300,7 @@ Assume {
Type: IsS5(a_1) /\ IsS5(a_2) /\ IsS5(a_3) /\ is_sint32(a_1.F5_a) /\
is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
(* Initializer *)
Init: forall i : Z. let a_4 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
(((a_4.F5_a) = 0) /\ ((a_4.F5_b) = 0) /\ ((a_4.F5_c) = 0)))).
@@ -329,7 +329,7 @@ Assume {
is_sint32(a_1.F5_a) /\ is_sint32(x_2) /\ is_sint32(x_1) /\
is_sint32(x).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
(* Initializer *)
Init: forall i : Z. let a_2 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
(((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
@@ -358,7 +358,7 @@ Assume {
Type: IsS5(a_1) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(x_3) /\
is_sint32(x_2) /\ is_sint32(x_1) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
(* Initializer *)
Init: forall i : Z. let a_2 = ts1_0[i] in ((0 <= i) -> ((i <= 1) ->
(((a_2.F5_a) = 0) /\ ((a_2.F5_b) = 0) /\ ((a_2.F5_c) = 0)))).
@@ -402,10 +402,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -512,10 +511,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -622,10 +620,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -733,10 +730,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -844,10 +840,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a_8).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -954,10 +949,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1064,10 +1058,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1175,10 +1168,9 @@ Assume {
is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\ is_sint32(a_1) /\
is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1285,10 +1277,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1395,10 +1386,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1505,10 +1495,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1616,10 +1605,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1726,10 +1714,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Goal *)
When: (0 <= i) /\ (i <= 31) /\ is_sint32(i).
(* Initializer *)
@@ -1839,10 +1826,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_8) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -1950,10 +1936,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_8) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -2060,10 +2045,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Goal *)
When: (0 <= i) /\ (i <= 3).
(* Initializer *)
@@ -2173,10 +2157,9 @@ Assume {
is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\ is_sint32(a_1) /\
is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
@@ -2283,10 +2266,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Goal *)
When: (6 <= i) /\ (i <= 6).
(* Initializer *)
@@ -2395,10 +2377,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Goal *)
When: (7 <= i) /\ (i <= 9).
(* Initializer *)
@@ -2507,10 +2488,9 @@ Assume {
is_sint32(a_6) /\ is_sint32(a_7[1]) /\ is_sint32(a_7[2]) /\
is_sint32(a_1) /\ is_sint32(a[5]).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS1_S(s) /\ IsS2_St(st_0) /\
- IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\
- IsS3_Sc(sq0_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS1_S(s) /\ IsS2_St(st_0) /\ IsS3_Sc(sc0_0) /\ IsS3_Sc(sc1_0) /\
+ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsS3_Sc(sq0_0) /\ IsU4_U(u).
(* Initializer *)
Init: x_5 = (-1).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
index 9501f9dee9b..5f0846a76ea 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
@@ -14,7 +14,7 @@ Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
is_sint32(ta1_0[4]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
}
Prove: (x_1 = x) /\ (x_2 = x_1).
@@ -26,7 +26,7 @@ Assume {
Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(ta1_0[3]) /\
is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
}
Prove: x = 0.
@@ -38,7 +38,7 @@ Assume {
Type: is_sint32(ta1_0[0]) /\ is_sint32(ta1_0[1]) /\ is_sint32(x) /\
is_sint32(ta1_0[4]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0).
+ Type: IsArray_sint32(ta1_0).
}
Prove: x = 1.
@@ -54,7 +54,7 @@ Let x_2 = ta2_0[4].
Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
}
Prove: (x_1 = x) /\ (x_2 = x_1).
@@ -65,7 +65,7 @@ Let x = ta2_0[4].
Assume {
Type: is_sint32(ta2_0[0]) /\ is_sint32(ta2_0[1]) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
}
Prove: x = 1.
@@ -76,7 +76,7 @@ Let x = ta2_0[1].
Assume {
Type: is_sint32(ta2_0[0]) /\ is_sint32(x) /\ is_sint32(ta2_0[4]).
(* Heap *)
- Type: IsArray1_sint32(ta2_0).
+ Type: IsArray_sint32(ta2_0).
}
Prove: x = 1.
@@ -94,8 +94,8 @@ Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(ta2_0[4]) /\
is_sint32(x_2) /\ is_sint32(x_3).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
}
Prove: (x_1 = x) /\ (x_3 = x_2).
@@ -107,8 +107,8 @@ Assume {
Type: is_sint32(ta1_0[2]) /\ is_sint32(ta1_0[4]) /\ is_sint32(ta2_0[4]) /\
is_sint32(x) /\ is_sint32(ta3_0[2]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
}
Prove: x = 1.
@@ -120,8 +120,8 @@ Assume {
Type: is_sint32(ta1_0[2]) /\ is_sint32(ta1_0[4]) /\ is_sint32(ta2_0[4]) /\
is_sint32(ta3_0[0]) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
}
Prove: x = 1.
@@ -133,8 +133,8 @@ Assume {
Type: is_sint32(ta1_0[2]) /\ is_sint32(ta1_0[4]) /\ is_sint32(x) /\
is_sint32(ta3_0[0]) /\ is_sint32(ta3_0[2]).
(* Heap *)
- Type: IsArray1_sint32(ta1_0) /\ IsArray1_sint32(ta2_0) /\
- IsArray1_sint32(ta3_0).
+ Type: IsArray_sint32(ta1_0) /\ IsArray_sint32(ta2_0) /\
+ IsArray_sint32(ta3_0).
}
Prove: x = 1.
@@ -154,7 +154,7 @@ Assume {
Type: IsS5(a) /\ IsS5(a_1) /\ IsS5(a_2) /\ is_sint32(a.F5_a) /\
is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(a_3.F5_c).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
}
Prove: (x_1 = x) /\ EqS5(a, a_1) /\ EqS5(a_1, a_2).
@@ -168,7 +168,7 @@ Assume {
Type: IsS5(a) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(a.F5_a) /\
is_sint32(a_1.F5_a) /\ is_sint32(a_1.F5_b) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
}
Prove: x = 1.
@@ -182,7 +182,7 @@ Assume {
Type: IsS5(a) /\ IsS5(ts1_0[1]) /\ IsS5(ts1_0[3]) /\ is_sint32(x) /\
is_sint32(a_1.F5_a) /\ is_sint32(a_1.F5_b) /\ is_sint32(a_1.F5_c).
(* Heap *)
- Type: IsArray1S5(ts1_0).
+ Type: IsArray_S5(ts1_0).
}
Prove: x = 1.
@@ -204,9 +204,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -271,9 +270,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -338,9 +336,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -406,9 +403,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -473,9 +469,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -541,9 +536,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -609,9 +603,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -677,9 +670,8 @@ Assume {
is_sint64(x_1) /\ is_sint16((u.F4_U_t)[0]) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
@@ -745,9 +737,8 @@ Assume {
is_sint64(u.F4_U_b) /\ is_sint16(a_5) /\ is_sint32(a_4) /\
is_sint32(a_1).
(* Heap *)
- Type: IsArray1_sint32(t) /\ IsArray1_sint32(t1_0) /\
- IsArray1_uint8(tab_0) /\ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\
- IsS3_Sc(sc3_0) /\ IsU4_U(u).
+ Type: IsArray_sint32(t) /\ IsArray_sint32(t1_0) /\ IsArray_uint8(tab_0) /\
+ IsS2_St(st_0) /\ IsS3_Sc(sc2_0) /\ IsS3_Sc(sc3_0) /\ IsU4_U(u).
(* Initializer *)
Init: (u.F4_U_a) = (-1).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index b941722cdbd..cebaff887df 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -41,7 +41,7 @@ Goal Post-condition (file tests/wp_acsl/logic.i, line 21) in 'h':
Let a = global(G_t_29).
Let m = Array1_S1(shift_S1(a, 0), 3, Mint_0).
Let m_1 = Array1_S1(a, 3, Mint_0).
-Assume { Type: IsArray1S1(m_1) /\ IsArray1S1(m). (* Call 'f' *) Have: P_P(m).
+Assume { Type: IsArray_S1(m_1) /\ IsArray_S1(m). (* Call 'f' *) Have: P_P(m).
}
Prove: P_P(m_1).
@@ -72,7 +72,7 @@ Let a_2 = shift_S1(a, 1).
Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
- Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
+ Type: IsArray_S1(m) /\ IsArray_S1(Array1_S1(a_3, 3, Mint_0)).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -97,7 +97,7 @@ Let a_2 = shift_S1(a, 1).
Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a, 3, Mint_0).
Assume {
- Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
+ Type: IsArray_S1(m) /\ IsArray_S1(Array1_S1(a_3, 3, Mint_0)).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -122,7 +122,7 @@ Let a_2 = shift_S1(a, 1).
Let a_3 = shift_S1(a, 0).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
+ Type: IsArray_S1(Array1_S1(a, 3, Mint_0)) /\ IsArray_S1(m).
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
index 43d8c4d3ece..02cc1e7481d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/record.res.oracle
@@ -50,7 +50,7 @@ Prove: true.
Goal Post-condition 'P2,qed_ok' in 'f':
Assume {
- Type: IsArray1_sint32(t1_0) /\ IsArray1_sint32(t2_0).
+ Type: IsArray_sint32(t1_0) /\ IsArray_sint32(t2_0).
(* Goal *)
When: forall i : Z. ((0 <= i) -> ((i <= 9) -> (t2_0[i] = t1_0[i]))).
}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
index fcb5d4edc86..28eb004ea32 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts788.res.oracle
@@ -16,7 +16,7 @@ Let x = t20_0[1].
Assume {
Type: is_sint32(x) /\ is_sint32(t20_0[2]).
(* Heap *)
- Type: IsArray1_sint32(t20_0).
+ Type: IsArray_sint32(t20_0).
(* Initializer *)
Init: t20_0[0] = 3.
(* Initializer *)
@@ -31,7 +31,7 @@ Let x = t20_0[2].
Assume {
Type: is_sint32(t20_0[1]) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(t20_0).
+ Type: IsArray_sint32(t20_0).
(* Initializer *)
Init: t20_0[0] = 3.
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
index 9875c8c8f67..d53c4143c88 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
@@ -14,8 +14,8 @@ Let a_2 = shift_sint32(a, j).
Let m = Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x].
Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\
- IsArray1_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
- IsArray1_sint32(Array1_int(a, 10, m)).
+ IsArray_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
+ IsArray_sint32(Array1_int(a, 10, m)).
(* Pre-condition *)
Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
}
@@ -32,8 +32,8 @@ Let a_2 = shift_sint32(a, j).
Let m_1 = Array1_int(a, 10,
Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x]).
Assume {
- Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\ IsArray1_sint32(m) /\
- is_sint32(x) /\ IsArray1_sint32(m_1).
+ Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\ IsArray_sint32(m) /\
+ is_sint32(x) /\ IsArray_sint32(m_1).
(* Pre-condition *)
Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
}
@@ -50,8 +50,8 @@ Let m = Array1_int(a, 10,
Mint_0[a_1 <- Mint_0[a_2]][a_2 <- x][shift_sint32(a, k) <- x]).
Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\
- IsArray1_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
- IsArray1_sint32(m).
+ IsArray_sint32(Array1_int(a, 10, Mint_0)) /\ is_sint32(x) /\
+ IsArray_sint32(m).
(* Pre-condition *)
Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
}
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index d6202c41035..ef6f162dd9a 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -133,7 +133,7 @@ Prove: true.
Goal Post-condition 'Preset_5' in 'call_reset_5':
Assume {
(* Heap *)
- Type: IsArray1S1_T(ts_1).
+ Type: IsArray_S1_T(ts_1).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'reset_5' *)
@@ -170,7 +170,7 @@ Goal Post-condition 'Presset_mat' in 'call_reset_5_dim2':
Let m = smatrix_0[1].
Assume {
(* Heap *)
- Type: IsArray2S1_T(smatrix_1).
+ Type: IsArray_d2_S1_T(smatrix_1).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'reset_5' *)
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
index e9a8a909640..aeb64156ce6 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
@@ -10,7 +10,7 @@ Goal Post-condition (file tests/wp_hoare/reference_array.i, line 49) in 'add_1_5
Let a = shift_A5_sint32(ap_0, 0).
Assume {
(* Heap *)
- Type: (region(ap_0.base) <= 0) /\ IsArray1_sint32(reg_load_0) /\
+ Type: (region(ap_0.base) <= 0) /\ IsArray_sint32(reg_load_0) /\
linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
@@ -46,7 +46,7 @@ Prove: true.
Goal Post-condition 'Pload' in 'calls_on_array_dim_1':
Assume {
(* Heap *)
- Type: IsArray1_sint32(t).
+ Type: IsArray_sint32(t).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
@@ -68,7 +68,7 @@ Prove: t[i] = reg_load_0[i].
Goal Post-condition 'Preset' in 'calls_on_array_dim_1':
Assume {
(* Heap *)
- Type: IsArray1_sint32(t_1).
+ Type: IsArray_sint32(t_1).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
@@ -90,7 +90,7 @@ Prove: t[i] = 0.
Goal Post-condition 'Padd' in 'calls_on_array_dim_1':
Assume {
(* Heap *)
- Type: IsArray1_sint32(t).
+ Type: IsArray_sint32(t).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
@@ -144,7 +144,7 @@ Goal Post-condition 'Pload' in 'calls_on_array_dim_2':
Let m = tt_0[0].
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_0).
+ Type: IsArray_d2_sint32(tt_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_1_5' *)
@@ -163,7 +163,7 @@ Prove: m[i] = reg_load_0[i].
Goal Post-condition 'Preset' in 'calls_on_array_dim_2':
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_0).
+ Type: IsArray_d2_sint32(tt_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_1_5' *)
@@ -183,7 +183,7 @@ Goal Post-condition 'Padd' in 'calls_on_array_dim_2':
Let m = tt_0[0].
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_0).
+ Type: IsArray_d2_sint32(tt_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_1_5' *)
@@ -235,7 +235,7 @@ Let m = tt_1[0].
Let m_1 = tt_0[0].
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_0).
+ Type: IsArray_d2_sint32(tt_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
@@ -257,7 +257,7 @@ Goal Post-condition 'Preset' in 'calls_on_array_dim_2_to_1':
Let m = tt_0[0].
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_1).
+ Type: IsArray_d2_sint32(tt_1).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
@@ -280,7 +280,7 @@ Let m = tt_1[0].
Let m_1 = tt_0[0].
Assume {
(* Heap *)
- Type: IsArray2_sint32(tt_0).
+ Type: IsArray_d2_sint32(tt_0).
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
index 46f3cde2efb..88e29f14f68 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const.res.oracle
@@ -16,7 +16,7 @@ Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
is_sint32(x_4).
(* Heap *)
- Type: IsArray1_sint32(A).
+ Type: IsArray_sint32(A).
}
Prove: x_4 = 6.
@@ -35,7 +35,7 @@ Prove: true.
Goal Post-condition 'KO' in 'fC':
Let x = A[3].
-Assume { Type: is_sint32(x). (* Heap *) Type: IsArray1_sint32(A). }
+Assume { Type: is_sint32(x). (* Heap *) Type: IsArray_sint32(A). }
Prove: x = 0.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
index 1ac8bbc1f3f..03f12a3394f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/injector.res.oracle
@@ -91,7 +91,7 @@ Let x_1 = inp_0[0].
Assume {
Type: is_sint32(b) /\ is_sint32(v) /\ is_sint32(x_1) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1_sint32(inp_1) /\ IsArray1_sint32(out_0).
+ Type: IsArray_sint32(inp_1) /\ IsArray_sint32(out_0).
If x != 33
Then { Have: inp_1[0 <- v] = inp_0. }
Else { (* Call Effects *) Have: inp_1[0 <- v][1 <- b] = inp_0. }
@@ -106,7 +106,7 @@ Prove: x_1 = b.
Goal Post-condition for 'ko_1' 'qed_ko' in 'f':
Assume {
(* Heap *)
- Type: IsArray1_sint32(out_0).
+ Type: IsArray_sint32(out_0).
(* Pre-condition for 'ko_1' *)
Have: out_0[0] = 33.
(* Pre-condition for 'ko_1' *)
@@ -120,7 +120,7 @@ Goal Post-condition for 'ko_1' 'qed_ko' in 'f':
Assume {
Type: is_sint32(b) /\ is_sint32(v).
(* Heap *)
- Type: IsArray1_sint32(out_0).
+ Type: IsArray_sint32(out_0).
(* Pre-condition for 'ko_1' *)
Have: out_0[0] = 33.
(* Pre-condition for 'ko_1' *)
@@ -133,7 +133,7 @@ Prove: v = b.
Goal Post-condition for 'ko_1' 'qed_ko' in 'f':
Assume {
(* Heap *)
- Type: IsArray1_sint32(out_0).
+ Type: IsArray_sint32(out_0).
(* Pre-condition for 'ko_1' *)
Have: out_0[0] = 33.
(* Pre-condition for 'ko_1' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
index 5392e0e5e2b..96f6ad55ed4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overarray.res.oracle
@@ -62,7 +62,7 @@ Goal Assigns nothing in 'f5_ko':
Call Effect at line 25
Assume {
(* Heap *)
- Type: IsArray1_sint32(A).
+ Type: IsArray_sint32(A).
(* Exit Effects *)
Have: forall i : Z. let x = 15 + i in (((-15) <= i) -> ((i <= 4) ->
(((i < 0) \/ (10 <= i)) -> (A_1[x] = A[x])))).
@@ -75,7 +75,7 @@ Goal Assigns nothing in 'f5_ko':
Call Effect at line 25
Assume {
(* Heap *)
- Type: IsArray1_sint32(A).
+ Type: IsArray_sint32(A).
(* Call Effects *)
Have: forall i : Z. let x = 15 + i in (((-15) <= i) -> ((i <= 4) ->
(((i < 0) \/ (10 <= i)) -> (A_1[x] = A[x])))).
@@ -91,7 +91,7 @@ Goal Assigns nothing in 'f6_ko':
Call Effect at line 28
Assume {
(* Heap *)
- Type: IsArray1_sint32(A).
+ Type: IsArray_sint32(A).
(* Exit Effects *)
Have: forall i : Z. let x = i - 5 in ((5 <= i) -> ((i <= 24) ->
(((i < 0) \/ (10 <= i)) -> (A_1[x] = A[x])))).
@@ -104,7 +104,7 @@ Goal Assigns nothing in 'f6_ko':
Call Effect at line 28
Assume {
(* Heap *)
- Type: IsArray1_sint32(A).
+ Type: IsArray_sint32(A).
(* Call Effects *)
Have: forall i : Z. let x = i - 5 in ((5 <= i) -> ((i <= 24) ->
(((i < 0) \/ (10 <= i)) -> (A_1[x] = A[x])))).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index 6911b721195..478d90b93f1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -11,7 +11,7 @@
Goal Assertion (file tests/wp_typed/array_initialized.c, line 71):
Assume {
(* Heap *)
- Type: IsArray1_sint32(g).
+ Type: IsArray_sint32(g).
(* Goal *)
When: (0 <= i) /\ (i <= 499).
(* Initializer *)
@@ -27,7 +27,7 @@ Prove: g[i] = 0.
Goal Assertion (file tests/wp_typed/array_initialized.c, line 185):
Assume {
(* Heap *)
- Type: IsArray1_sint32(h1_0) /\ IsArray1_sint32(h2_0).
+ Type: IsArray_sint32(h1_0) /\ IsArray_sint32(h2_0).
(* Goal *)
When: (0 <= i) /\ (i <= 499).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
index ff1c02a4ba5..e433d6edd6b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
@@ -10,7 +10,7 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
Assume {
Type: is_sint32(k).
(* Heap *)
- Type: IsArray1S1(comp_0) /\
+ Type: IsArray_S1(comp_0) /\
(forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
@@ -26,7 +26,7 @@ Let x = Mint_0[a <- 4][a_1].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1S1(comp_0) /\
+ Type: IsArray_S1(comp_0) /\
(forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
index 93b72601618..f958319c4c3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
@@ -10,7 +10,7 @@ Goal Assertion 'SEP' (file tests/wp_typed/frame.i, line 10):
Assume {
Type: is_sint32(k).
(* Heap *)
- Type: IsArray1S1(comp_0) /\
+ Type: IsArray_S1(comp_0) /\
(forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
@@ -26,7 +26,7 @@ Let x = Mint_0[a <- 4][a_1].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
(* Heap *)
- Type: IsArray1S1(comp_0) /\
+ Type: IsArray_S1(comp_0) /\
(forall i : Z. region(comp_0[i].F1_ptr.base) <= 0).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 19).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index b7a091489fb..39eec2a7ec3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -11,7 +11,7 @@
Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
Assume {
(* Heap *)
- Type: IsArray1_sint8(A).
+ Type: IsArray_sint8(A).
(* Call 'Write' *)
Have: A[0] = 1.
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index a58a157b823..4baeb158a84 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -11,7 +11,7 @@
Goal Post-condition (file tests/wp_typed/mvar.i, line 12) in 'Job':
Assume {
(* Heap *)
- Type: IsArray1_sint8(A).
+ Type: IsArray_sint8(A).
(* Call 'Write' *)
Have: A[0] = 1.
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
index 5fcad89c141..d88f617e216 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
@@ -23,8 +23,7 @@ theory Matrix
(* use frama_c_wp.cint.Cint *)
- predicate IsArray1_sint32 (t:int -> int) =
- forall i:int. is_sint32 (get t i)
+ predicate IsArray_sint32 (t:int -> int) = forall i:int. is_sint32 (get t i)
end
---------------------------------------------
--- Context 'typed_f' Cluster 'S1_s'
@@ -50,9 +49,9 @@ theory S1_s
(* use Matrix *)
predicate IsS1_s (s:S1_s) =
- IsArray1_sint32 (F1_s_a s) /\ IsArray1_sint32 (F1_s_b s)
+ IsArray_sint32 (F1_s_a s) /\ IsArray_sint32 (F1_s_b s)
- predicate IsArray1S1_s (t:int -> S1_s) = forall i:int. IsS1_s (get t i)
+ predicate IsArray_S1_s (t:int -> S1_s) = forall i:int. IsS1_s (get t i)
end
[wp:print-generated]
theory WP
@@ -81,7 +80,7 @@ end
0 <= i ->
a1 < a2 ->
i <= 9 ->
- IsArray1S1_s t ->
+ IsArray_S1_s t ->
is_uint32 i ->
is_sint32 a2 ->
is_sint32 a1 -> is_sint32 ((1 + ((- 1) * a1)) + a3) -> (2 * a1) <= a3
@@ -100,7 +99,7 @@ Assume {
Type: is_uint32(SynchroId_0) /\ is_sint32(a_2) /\ is_sint32(a_1) /\
is_sint32(1 + a_3 - a_1).
(* Heap *)
- Type: IsArray1S1_s(t).
+ Type: IsArray_S1_s(t).
(* Residual *)
When: a_1 < a_2.
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
index f3cb015dea5..d0e98a6c7f4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.0.res.oracle
@@ -13,7 +13,7 @@ Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(d) /\
is_sint32(x).
(* Heap *)
- Type: IsArray2_sint32(t).
+ Type: IsArray_d2_sint32(t).
(* Goal *)
When: c != a.
}
@@ -33,7 +33,7 @@ Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(d) /\
is_sint32(x).
(* Heap *)
- Type: IsArray2_sint32(t).
+ Type: IsArray_d2_sint32(t).
}
Prove: x = 1.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
index c0f6bc8b083..bb1396ee3af 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_matrix.1.res.oracle
@@ -13,7 +13,7 @@ Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(d) /\
is_sint32(x).
(* Heap *)
- Type: IsArray2_sint32(t).
+ Type: IsArray_d2_sint32(t).
(* Goal *)
When: c != a.
}
@@ -33,7 +33,7 @@ Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(d) /\
is_sint32(x).
(* Heap *)
- Type: IsArray2_sint32(t).
+ Type: IsArray_d2_sint32(t).
}
Prove: x = 1.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 08ed2413253..111dc92f510 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -16,9 +16,9 @@ Let x = k - 1.
Let m = p[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(v_1) /\
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(v_1) /\
is_sint32(v) /\ is_sint32(x1_0) /\ is_sint32(x2_0) /\ is_sint32(x) /\
- is_sint32(1 + k) /\ IsArray1_sint32(m) /\ IsArray1_sint32(m_1).
+ is_sint32(1 + k) /\ IsArray_sint32(m) /\ IsArray_sint32(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
@@ -35,9 +35,9 @@ Let x = k - 1.
Let m = p[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(v) /\
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(v) /\
is_sint32(v_1) /\ is_sint32(x1_0) /\ is_sint32(x2_0) /\ is_sint32(x) /\
- is_sint32(1 + k) /\ IsArray1_sint32(m) /\ IsArray1_sint32(m_1).
+ is_sint32(1 + k) /\ IsArray_sint32(m) /\ IsArray_sint32(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
@@ -61,8 +61,8 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in
:
Let m = p[k <- v].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
- IsArray1_sint32(m) /\ is_sint32(1 + k).
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
+ IsArray_sint32(m) /\ is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job' *)
@@ -85,9 +85,9 @@ Let x = k - 1.
Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -104,9 +104,9 @@ Let x = k - 1.
Let m = q[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
IsS1_S(v_1) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -124,9 +124,9 @@ Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Let m_2 = q[x <- s1_0].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -150,7 +150,7 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in
:
Let m = q[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray1S1_S(m) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
@@ -174,9 +174,9 @@ Let x = k - 1.
Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -193,9 +193,9 @@ Let x = k - 1.
Let m = q[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
IsS1_S(v_1) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -213,9 +213,9 @@ Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Let m_2 = q[x <- s1_0].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -239,7 +239,7 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in
:
Let m = q[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray1S1_S(m) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
@@ -322,7 +322,7 @@ Goal Post-condition 'Q' in 'job3':
Let a = s.F1_S_f.
Let m = q[k <- { F1_S_f = (q[k].F1_S_f)[0 <- a[0]][1 <- a[1]] }].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s) /\ is_sint32(k) /\ IsArray1S1_S(m).
+ Type: IsArray_S1_S(q) /\ IsS1_S(s) /\ is_sint32(k) /\ IsArray_S1_S(m).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 9).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index af4d14ff9c3..1b950374764 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -16,9 +16,9 @@ Let x = k - 1.
Let m = p[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(v_1) /\
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(v_1) /\
is_sint32(v) /\ is_sint32(x1_0) /\ is_sint32(x2_0) /\ is_sint32(x) /\
- is_sint32(1 + k) /\ IsArray1_sint32(m) /\ IsArray1_sint32(m_1).
+ is_sint32(1 + k) /\ IsArray_sint32(m) /\ IsArray_sint32(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
@@ -35,9 +35,9 @@ Let x = k - 1.
Let m = p[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(v) /\
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(v) /\
is_sint32(v_1) /\ is_sint32(x1_0) /\ is_sint32(x2_0) /\ is_sint32(x) /\
- is_sint32(1 + k) /\ IsArray1_sint32(m) /\ IsArray1_sint32(m_1).
+ is_sint32(1 + k) /\ IsArray_sint32(m) /\ IsArray_sint32(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job' *)
@@ -61,8 +61,8 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in
:
Let m = p[k <- v].
Assume {
- Type: IsArray1_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
- IsArray1_sint32(m) /\ is_sint32(1 + k).
+ Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
+ IsArray_sint32(m) /\ is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
(* Call 'job' *)
@@ -85,9 +85,9 @@ Let x = k - 1.
Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -104,9 +104,9 @@ Let x = k - 1.
Let m = q[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
IsS1_S(v_1) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -124,9 +124,9 @@ Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Let m_2 = q[x <- s1_0].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job2' *)
@@ -150,7 +150,7 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in
:
Let m = q[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray1S1_S(m) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
@@ -174,9 +174,9 @@ Let x = k - 1.
Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -193,9 +193,9 @@ Let x = k - 1.
Let m = q[x <- v_1].
Let m_1 = m[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v) /\
IsS1_S(v_1) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -213,9 +213,9 @@ Let m = q[x <- v].
Let m_1 = m[k <- v_1].
Let m_2 = q[x <- s1_0].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ IsS1_S(s2_0) /\ IsS1_S(v_1) /\
IsS1_S(v) /\ is_sint32(k) /\ is_sint32(x) /\ is_sint32(1 + k) /\
- IsArray1S1_S(m) /\ IsArray1S1_S(m_1).
+ IsArray_S1_S(m) /\ IsArray_S1_S(m_1).
(* Pre-condition *)
Have: (0 < k) /\ (k <= 9).
(* Call 'job3' *)
@@ -239,7 +239,7 @@ Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in
:
Let m = q[k <- v].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray1S1_S(m) /\
+ Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
is_sint32(1 + k).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 8).
@@ -322,7 +322,7 @@ Goal Post-condition 'Q' in 'job3':
Let a = s.F1_S_f.
Let m = q[k <- { F1_S_f = (q[k].F1_S_f)[0 <- a[0]][1 <- a[1]] }].
Assume {
- Type: IsArray1S1_S(q) /\ IsS1_S(s) /\ is_sint32(k) /\ IsArray1S1_S(m).
+ Type: IsArray_S1_S(q) /\ IsS1_S(s) /\ is_sint32(k) /\ IsArray_S1_S(m).
(* Pre-condition *)
Have: (0 <= k) /\ (k <= 9).
}
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 57d9150a815..e1453e78f00 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
@@ -795,7 +795,7 @@ Prove: true.
Goal Post-condition (file tests/wp_typed/user_init.i, line 39) in 'init_t2_v1':
Assume {
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -816,7 +816,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -855,7 +855,7 @@ Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -893,7 +893,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
(* Loop assigns 'lack,Zone_i' *)
@@ -937,7 +937,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_2).
+ Type: IsArray_d2_sint32(t2_2).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -980,7 +980,7 @@ Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1037,7 +1037,7 @@ Effect at line 51
Assume {
Type: is_uint32(i_2).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1076,7 +1076,7 @@ Effect at line 58
Assume {
Type: is_uint32(i_2).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1120,7 +1120,7 @@ Effect at line 58
Assume {
Type: is_uint32(i_2) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1162,7 +1162,7 @@ Effect at line 59
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -1211,7 +1211,7 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
@@ -1227,7 +1227,7 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 5
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1264,7 +1264,7 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 5
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1680,8 +1680,8 @@ Prove: P_MemSet20(t2_0[i], 20, v).
Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
(* Invariant 'Partial_i' *)
@@ -1705,8 +1705,8 @@ Prove: true.
Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1729,8 +1729,8 @@ Prove: true.
Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
Let m = v[j <- v_1].
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]) /\ IsArray_sint32(m).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1752,7 +1752,7 @@ Prove: P_MemSet20(m, to_uint32(1 + j), v_1).
Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
Let m = t2_0[i].
Assume {
- Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
+ Type: is_uint32(i) /\ is_sint32(v) /\ IsArray_sint32(m).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v))).
@@ -1767,8 +1767,8 @@ Prove: P_MemSet20(m, 0, v).
Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1810,8 +1810,8 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 111
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i_2]).
+ Type: IsArray_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i_2]).
(* Goal *)
When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
(i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
@@ -1833,8 +1833,8 @@ Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
Goal Loop assigns 'tactic,Zone_i' (3/3):
Effect at line 117
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
(* Invariant 'Partial_i' *)
@@ -1884,8 +1884,8 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1907,8 +1907,8 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
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 2b7c224c04f..52e4c648900 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
@@ -795,7 +795,7 @@ Prove: true.
Goal Post-condition (file tests/wp_typed/user_init.i, line 39) in 'init_t2_v1':
Assume {
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -816,7 +816,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i_1) /\ (0 <= i_2) /\ (i_1 < to_uint32(1 + i)) /\ (i_2 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -855,7 +855,7 @@ Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -893,7 +893,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_1).
+ Type: IsArray_d2_sint32(t2_1).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + j)).
(* Loop assigns 'lack,Zone_i' *)
@@ -937,7 +937,7 @@ Let m = t2_0[i].
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_2).
+ Type: IsArray_d2_sint32(t2_2).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i) /\ (0 <= i_2) /\ (i_2 <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -980,7 +980,7 @@ Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1037,7 +1037,7 @@ Effect at line 51
Assume {
Type: is_uint32(i_2).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1076,7 +1076,7 @@ Effect at line 58
Assume {
Type: is_uint32(i_2).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1120,7 +1120,7 @@ Effect at line 58
Assume {
Type: is_uint32(i_2) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
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) /\
@@ -1162,7 +1162,7 @@ Effect at line 59
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Goal *)
When: (0 <= i) /\ (0 <= j) /\ (i <= 9) /\ (j <= 19).
(* Loop assigns 'lack,Zone_i' *)
@@ -1211,7 +1211,7 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
@@ -1227,7 +1227,7 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 5
Assume {
Type: is_uint32(i).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1264,7 +1264,7 @@ Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 5
Assume {
Type: is_uint32(i) /\ is_uint32(j).
(* Heap *)
- Type: IsArray2_sint32(t2_0).
+ Type: IsArray_d2_sint32(t2_0).
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((0 <= i_1) -> ((i_2 <= 9) ->
((i_1 <= 19) ->
@@ -1680,8 +1680,8 @@ Prove: P_MemSet20(t2_0[i], 20, v).
Goal Preservation of Invariant 'Partial_i' (file tests/wp_typed/user_init.i, line 108):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint32(1 + i)).
(* Invariant 'Partial_i' *)
@@ -1705,8 +1705,8 @@ Prove: true.
Goal Preservation of Invariant 'Range_i' (file tests/wp_typed/user_init.i, line 107):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1729,8 +1729,8 @@ Prove: true.
Goal Preservation of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
Let m = v[j <- v_1].
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]) /\ IsArray1_sint32(m).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]) /\ IsArray_sint32(m).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1752,7 +1752,7 @@ Prove: P_MemSet20(m, to_uint32(1 + j), v_1).
Goal Establishment of Invariant 'Partial_j' (file tests/wp_typed/user_init.i, line 114):
Let m = t2_0[i].
Assume {
- Type: is_uint32(i) /\ is_sint32(v) /\ IsArray1_sint32(m).
+ Type: is_uint32(i) /\ is_sint32(v) /\ IsArray_sint32(m).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v))).
@@ -1767,8 +1767,8 @@ Prove: P_MemSet20(m, 0, v).
Goal Preservation of Invariant 'Range_j' (file tests/wp_typed/user_init.i, line 113):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1810,8 +1810,8 @@ Prove: true.
Goal Loop assigns 'tactic,Zone_i' (2/3):
Effect at line 111
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i_2]).
+ Type: IsArray_sint32(v) /\ is_uint32(i_2) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i_2]).
(* Goal *)
When: (0 <= i_3) /\ (0 <= i_4) /\ (0 <= i_5) /\ (0 <= i) /\ (i_3 <= 9) /\
(i_5 <= 9) /\ (i <= 9) /\ (i_4 <= 19).
@@ -1833,8 +1833,8 @@ Prove: exists i_7,i_6 : Z. (i_7 <= i) /\ (i_6 <= i_1) /\ (0 <= i_7) /\
Goal Loop assigns 'tactic,Zone_i' (3/3):
Effect at line 117
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Goal *)
When: (0 <= i) /\ (0 <= i_1) /\ (i <= 9) /\ (i_1 <= 19).
(* Invariant 'Partial_i' *)
@@ -1884,8 +1884,8 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 111):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
- IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_sint32(v_1) /\
+ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
@@ -1907,8 +1907,8 @@ Prove: true.
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 117):
Assume {
- Type: IsArray1_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
- is_sint32(v_1) /\ IsArray1_sint32(t2_0[i]).
+ Type: IsArray_sint32(v) /\ is_uint32(i) /\ is_uint32(j) /\
+ is_sint32(v_1) /\ IsArray_sint32(t2_0[i]).
(* Invariant 'Partial_i' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
P_MemSet20(t2_0[i_1], 20, v_1))).
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index a9966d41d85..b729e0fa942 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0196,
+ "verdict": "valid", "time": 0.0169,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0223,
+ "verdict": "valid", "time": 0.0167,
"steps": 39 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 0be61590020..2580abd19c2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0152,
+ "verdict": "valid", "time": 0.0146,
"steps": 27 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0151,
+ "verdict": "valid", "time": 0.0146,
"steps": 27 } ] } } ]
--
GitLab