Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
90676872
Commit
90676872
authored
Oct 15, 2020
by
Loïc Correnson
Browse files
[wp] renamed is-array predicates
parent
2f39567a
Changes
31
Hide whitespace changes
Inline
Side-by-side
src/plugins/wp/Cvalues.ml
View file @
90676872
...
...
@@ -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
t
e
Format
.
asprintf
"%sArray%
a_
%s"
C
.
prefix
pp_dim
dim
(
Lang
.
comp_id
c
)
|
C_float
_
|
C_pointer
_
|
C_array
_
->
assert
fals
e
let
rec
is_obj
obj
t
=
match
obj
with
...
...
src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
View file @
90676872
...
...
@@ -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: IsArray
1
_sint32(t2_0) /\ IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_sint32(t4_0).
Type: IsArray_sint32(t4_0).
(* Goal *)
When: 0 <= j.
(* Pre-condition *)
...
...
src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
View file @
90676872
...
...
@@ -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: IsArray
1
_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) /\
...
...
src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
View file @
90676872
...
...
@@ -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: IsArray
1
_sint32(t0_0) /\ IsArray
1
_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) /\ IsArray
1
_sint32(a) /\
IsArray
1
_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) /\ IsArray
1
_sint32(a_4) /\
IsArray
1
_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 *)
...
...
src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.0.res.oracle
View file @
90676872
...
...
@@ -26,7 +26,7 @@ Let x = G[0].
Assume {
Type: is_sint32(i) /\ is_sint32(x) /\ is_sint32(G[1]).
(* Heap *)
Type: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_sint32(G).
Type: IsArray_sint32(G).
(* Goal *)
When: (x != 0) /\ (G[1] = 0).
If i <= 3
...
...
src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
View file @
90676872
...
...
@@ -10,7 +10,7 @@
Goal Post-condition 'KO' in 'extra':
Let x = A[2].
Assume { Type: is_sint32(x). (* Heap *) Type: IsArray
1
_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: IsArray
1
_sint32(A) /\ IsArray
1
_sint32(A_1) /\ is_sint32(x).
Type: IsArray_sint32(A) /\ IsArray_sint32(A_1) /\ is_sint32(x).
(* Initializer *)
Init: A_1[0] = 10.
(* Initializer *)
...
...
src/plugins/wp/tests/wp_acsl/oracle/init_value.0.res.oracle
View file @
90676872
...
...
@@ -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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\
IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\
IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\
IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\
IsArray
1
_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: IsArray
1
S5(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: IsArray
1
S5(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: IsArray
1
S5(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 *)
...
...
src/plugins/wp/tests/wp_acsl/oracle/init_value.1.res.oracle
View file @
90676872
...
...
@@ -14,7 +14,7 @@ Assume {
Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
is_sint32(ta1_0[4]).
(* Heap *)
Type: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\
IsArray
1
_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: IsArray
1
_sint32(ta1_0) /\ IsArray
1
_sint32(ta2_0) /\