From ce445a3d24b6a132d737d285396244f52368e608 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 3 May 2022 15:00:30 +0200
Subject: [PATCH] [wp] tests oracles related to Why3 VC format
---
.../wp/tests/wp/oracle/sharing.res.oracle | 2 +-
.../oracle/chunk_typing_usable.res.oracle | 22 ++++-----
.../tests/wp_acsl/oracle/inductive.res.oracle | 30 ++++++------
.../oracle/predicates_functions.res.oracle | 5 +-
.../wp_acsl/oracle/struct_fields.res.oracle | 40 ++++++++--------
.../tests/wp_bts/oracle/bts_2110.res.oracle | 10 ++--
.../wp_plugin/oracle/inductive.res.oracle | 30 ++++++------
.../tests/wp_plugin/oracle/model.res.oracle | 4 +-
.../oracle/multi_matrix_types.res.oracle | 48 +++++++++----------
9 files changed, 96 insertions(+), 95 deletions(-)
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index b01d3e9c63e..efd2e9f9df7 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -57,7 +57,7 @@ end
let m3 = set m2 (shift_sint32 a 3) (get m2 a2) in
0 <= i1 ->
0 <= i ->
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
i1 <= 9 ->
i <= 9 ->
linked t ->
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index 58865eff22d..2067e2fba85 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -75,13 +75,13 @@ theory A_Occ
(* use Chunk *)
- Q_empty :
+ axiom Q_empty :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
(* use Compound *)
- Q_is :
+ axiom Q_is :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in
@@ -91,7 +91,7 @@ theory A_Occ
is_sint32 v ->
is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t
- Q_isnt :
+ axiom Q_isnt :
forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in
@@ -154,7 +154,7 @@ end
forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
i3 <= i1 ->
i < i3 ->
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
is_sint32_chunk t ->
is_uint32 i3 ->
is_uint32 i1 ->
@@ -233,14 +233,14 @@ theory A_Occ1
(* use Chunk1 *)
- Q_empty1 :
+ axiom Q_empty1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
t <=' f ->
is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
(* use Compound1 *)
- Q_is1 :
+ axiom Q_is1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in
@@ -250,7 +250,7 @@ theory A_Occ1
is_sint321 v ->
is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t
- Q_isnt1 :
+ axiom Q_isnt1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in
@@ -315,7 +315,7 @@ end
let x = (- 1) +' i1 in
not get1 t (shift_sint321 a x) = i2 ->
i <' i1 ->
- region1 (base1 a) <=' 0 ->
+ region1 (a.base1) <=' 0 ->
i1 <=' 1000 ->
is_sint32_chunk1 t ->
is_uint321 i1 ->
@@ -392,14 +392,14 @@ theory A_Occ2
(* use Chunk2 *)
- Q_empty2 :
+ axiom Q_empty2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
t <='' f ->
is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
(* use Compound2 *)
- Q_is2 :
+ axiom Q_is2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in
@@ -409,7 +409,7 @@ theory A_Occ2
is_sint322 v ->
is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t
- Q_isnt2 :
+ axiom Q_isnt2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 982b66a1342..4469b488143 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -138,42 +138,42 @@ end
forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin:int) (end1:int) =
+ addr) (begin1:int) (end1:int) =
forall i:int.
- begin <= i ->
+ begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin:int) (i:int) (j:int) (end1:int) =
+ (begin1:int) (i:int) (j:int) (end1:int) =
((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin <= i) /\
+ begin1 <= i) /\
i < j) /\
j < end1) /\
(forall i1:int.
not i1 = i ->
not j = i1 ->
- begin <= i1 ->
+ begin1 <= i1 ->
i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, end1:int.
- P_same_array mint mint1 a b begin end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_same_array mint mint1 a b begin1 end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, i:int, j:int, end1:int.
- P_swap mint mint1 a b begin i j end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_swap mint mint1 a b begin1 i j end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
- addr, b:addr, c:addr, begin:int, end1:int.
- P_same_elements mint mint1 b c begin end1 ->
- P_same_elements mint1 mint2 a b begin end1 ->
- P_same_elements mint mint2 a c begin end1
+ addr, b:addr, c:addr, begin1:int, end1:int.
+ P_same_elements mint mint1 b c begin1 end1 ->
+ P_same_elements mint1 mint2 a b begin1 end1 ->
+ P_same_elements mint mint2 a c begin1 end1
goal wp_goal :
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
index 67a25621bb8..fa26e5047b4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
@@ -22,13 +22,14 @@
predicate P_RP int
- P_RP_def : forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
+ axiom P_RP_def :
+ forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
function L_F (i:int) : int = 2 * i
function L_RF int : int
- L_RF_def :
+ axiom L_RF_def :
forall i:int. L_RF i = (if i <= 0 then 0 else L_F i + L_RF ((- 1) + i))
goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index aa0c5615572..df29522c76e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -89,13 +89,13 @@ theory Compound
Init_S1_X1 (get init (shiftfield_F1_X_a p))
(get init (shiftfield_F1_X_b p)) (get init (shiftfield_F1_X_c p))
- Q_Load_S1_X_update_Mchar0 :
+ axiom Q_Load_S1_X_update_Mchar0 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
separated p 3 q 1 ->
Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_eqmem_Mchar0 :
+ axiom Q_Load_S1_X_eqmem_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
@@ -104,21 +104,21 @@ theory Compound
eqmem mchar mchar1 q n ->
Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_havoc_Mchar0 :
+ axiom Q_Load_S1_X_havoc_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr
[Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
separated p 3 q n ->
- Load_S1_X p (havoc mchar1 mchar q n) mint mint1
- = Load_S1_X p mchar mint mint1
+ Load_S1_X p (havoc mchar1 mchar q n) mint mint1 =
+ Load_S1_X p mchar mint mint1
- Q_Load_S1_X_update_Mint1 :
+ axiom Q_Load_S1_X_update_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
separated p 3 q 1 ->
Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_eqmem_Mint1 :
+ axiom Q_Load_S1_X_eqmem_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
@@ -127,21 +127,21 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_havoc_Mint1 :
+ axiom Q_Load_S1_X_havoc_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
separated p 3 q n ->
- Load_S1_X p mchar (havoc mint2 mint1 q n) mint
- = Load_S1_X p mchar mint1 mint
+ Load_S1_X p mchar (havoc mint2 mint1 q n) mint =
+ Load_S1_X p mchar mint1 mint
- Q_Load_S1_X_update_Mint2 :
+ axiom Q_Load_S1_X_update_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
separated p 3 q 1 ->
Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_eqmem_Mint2 :
+ axiom Q_Load_S1_X_eqmem_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
@@ -150,28 +150,28 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
- Q_Load_S1_X_havoc_Mint2 :
+ axiom Q_Load_S1_X_havoc_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
separated p 3 q n ->
- Load_S1_X p mchar mint (havoc mint2 mint1 q n)
- = Load_S1_X p mchar mint mint1
+ Load_S1_X p mchar mint (havoc mint2 mint1 q n) =
+ Load_S1_X p mchar mint mint1
- Q_Load_Init_S1_X_update_Init0 :
+ axiom Q_Load_Init_S1_X_update_Init0 :
forall init:addr -> bool, p:addr, q:addr, v:bool
[Load_Init_S1_X p (set init q v)].
separated p 3 q 1 ->
Load_Init_S1_X p (set init q v) = Load_Init_S1_X p init
- Q_Load_Init_S1_X_eqmem_Init0 :
+ axiom Q_Load_Init_S1_X_eqmem_Init0 :
forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
[Load_Init_S1_X p init, eqmem init init1 q n| Load_Init_S1_X p init1,
eqmem init init1 q n].
included p 3 q n ->
eqmem init init1 q n -> Load_Init_S1_X p init1 = Load_Init_S1_X p init
- Q_Load_Init_S1_X_havoc_Init0 :
+ axiom Q_Load_Init_S1_X_havoc_Init0 :
forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
[Load_Init_S1_X p (havoc init1 init q n)].
separated p 3 q n ->
@@ -236,7 +236,7 @@ end
forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3:
addr -> int, t4:addr -> int, a:addr.
Load_Init_S1_X a t = x ->
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
@@ -272,7 +272,7 @@ end
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
addr -> int, a:addr, x:S1_X.
- region (base a) <= 0 ->
+ region (a.base) <= 0 ->
IsS1_X x ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index fe74a260b12..c8d3f169d3f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -59,19 +59,19 @@ theory Compound
function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0
- Q_Load_S2_A_update_Mint0 :
+ axiom Q_Load_S2_A_update_Mint0 :
forall mint:addr -> int, p:addr, q:addr, v:int
[Load_S2_A p (set mint q v)].
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
- Q_Load_S2_A_eqmem_Mint0 :
+ axiom Q_Load_S2_A_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
eqmem mint mint1 q n].
included p 1 q n ->
eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
- Q_Load_S2_A_havoc_Mint0 :
+ axiom Q_Load_S2_A_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p (havoc mint1 mint q n)].
separated p 1 q n ->
@@ -104,8 +104,8 @@ end
let a3 = Load_S2_A a t in
let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
not x = i ->
- region (base a1) <= 0 ->
- region (base a) <= 0 ->
+ region (a1.base) <= 0 ->
+ region (a.base) <= 0 ->
is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3
end
[wp] 1 goal generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 973a39e45fa..25cdbf437dc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -101,42 +101,42 @@ end
P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node
predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin:int) (end1:int) =
+ addr) (begin1:int) (end1:int) =
forall i:int.
- begin <= i ->
+ begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin:int) (i:int) (j:int) (end1:int) =
+ (begin1:int) (i:int) (j:int) (end1:int) =
((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin <= i) /\
+ begin1 <= i) /\
i < j) /\
j < end1) /\
(forall i1:int.
not i1 = i ->
not j = i1 ->
- begin <= i1 ->
+ begin1 <= i1 ->
i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, end1:int.
- P_same_array mint mint1 a b begin end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_same_array mint mint1 a b begin1 end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+ forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
int, i:int, j:int, end1:int.
- P_swap mint mint1 a b begin i j end1 ->
- P_same_elements mint mint1 a b begin end1
+ P_swap mint mint1 a b begin1 i j end1 ->
+ P_same_elements mint mint1 a b begin1 end1
| Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
- addr, b:addr, c:addr, begin:int, end1:int.
- P_same_elements mint mint1 b c begin end1 ->
- P_same_elements mint1 mint2 a b begin end1 ->
- P_same_elements mint mint2 a c begin end1
+ addr, b:addr, c:addr, begin1:int, end1:int.
+ P_same_elements mint mint1 b c begin1 end1 ->
+ P_same_elements mint1 mint2 a b begin1 end1 ->
+ P_same_elements mint mint2 a c begin1 end1
goal wp_goal :
forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 70fd22d935e..29f604c34ea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -74,7 +74,7 @@ end
goal wp_goal :
forall t:addr -> int, i:int, a:addr.
let x = get t (shift_sint32 a i) in
- region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+ region (a.base) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
end
[wp] 1 goal generated
------------------------------------------------------------
@@ -162,7 +162,7 @@ end
goal wp_goal :
forall t:addr1 -> int, i:int, a:addr1.
let x = get1 t (shift_sint321 a i) in
- region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
+ region1 (a.base1) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
end
[wp] 1 goal generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index 324a789c9b9..268995c9ffb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -103,61 +103,61 @@ theory Compound
(Array_uint32 (shiftfield_F1_S_a p) 5 mint)
(Array_sint64 (shiftfield_F1_S_b p) 5 mint2)
- Q_Array_uint32_access :
+ axiom Q_Array_uint32_access :
forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_uint32 p n mint) i].
0 <= i ->
i < n -> get (Array_uint32 p n mint) i = get mint (shift_uint32 p i)
- Q_Array_uint32_update_Mint0 :
+ axiom Q_Array_uint32_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_uint32 p n (set mint q v)].
not q = p -> Array_uint32 p n (set mint q v) = Array_uint32 p n mint
- Q_Array_uint32_eqmem_Mint0 :
+ axiom Q_Array_uint32_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_uint32 p n mint, eqmem mint mint1 q n1| Array_uint32 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_uint32 p n mint1 = Array_uint32 p n mint
- Q_Array_uint32_havoc_Mint0 :
+ axiom Q_Array_uint32_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_uint32 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
- Q_Array_sint64_access :
+ axiom Q_Array_sint64_access :
forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_sint64 p n mint) i].
0 <= i ->
i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p i)
- Q_Array_sint64_update_Mint0 :
+ axiom Q_Array_sint64_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_sint64 p n (set mint q v)].
not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint
- Q_Array_sint64_eqmem_Mint0 :
+ axiom Q_Array_sint64_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint
- Q_Array_sint64_havoc_Mint0 :
+ axiom Q_Array_sint64_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint64 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
- Q_Load_S1_S_update_Mint0 :
+ axiom Q_Load_S1_S_update_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
separated p 11 q 1 ->
Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2
- Q_Load_S1_S_eqmem_Mint0 :
+ axiom Q_Load_S1_S_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint mint2 mint3,
eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
@@ -166,21 +166,21 @@ theory Compound
eqmem mint mint1 q n ->
Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3
- Q_Load_S1_S_havoc_Mint0 :
+ axiom Q_Load_S1_S_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
separated p 11 q n ->
- Load_S1_S p (havoc mint1 mint q n) mint2 mint3
- = Load_S1_S p mint mint2 mint3
+ Load_S1_S p (havoc mint1 mint q n) mint2 mint3 =
+ Load_S1_S p mint mint2 mint3
- Q_Load_S1_S_update_Mint1 :
+ axiom Q_Load_S1_S_update_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
separated p 11 q 1 ->
Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint
- Q_Load_S1_S_eqmem_Mint1 :
+ axiom Q_Load_S1_S_eqmem_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint3 mint1 mint,
eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
@@ -189,21 +189,21 @@ theory Compound
eqmem mint1 mint2 q n ->
Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint
- Q_Load_S1_S_havoc_Mint1 :
+ axiom Q_Load_S1_S_havoc_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
separated p 11 q n ->
- Load_S1_S p mint3 (havoc mint2 mint1 q n) mint
- = Load_S1_S p mint3 mint1 mint
+ Load_S1_S p mint3 (havoc mint2 mint1 q n) mint =
+ Load_S1_S p mint3 mint1 mint
- Q_Load_S1_S_update_Mint2 :
+ axiom Q_Load_S1_S_update_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
separated p 11 q 1 ->
Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2
- Q_Load_S1_S_eqmem_Mint2 :
+ axiom Q_Load_S1_S_eqmem_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr [Load_S1_S p mint1 mint mint2,
eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
@@ -212,13 +212,13 @@ theory Compound
eqmem mint2 mint3 q n ->
Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2
- Q_Load_S1_S_havoc_Mint2 :
+ axiom Q_Load_S1_S_havoc_Mint2 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr
[Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
separated p 11 q n ->
- Load_S1_S p mint1 mint (havoc mint3 mint2 q n)
- = Load_S1_S p mint1 mint mint2
+ Load_S1_S p mint1 mint (havoc mint3 mint2 q n) =
+ Load_S1_S p mint1 mint mint2
end
[wp:print-generated]
theory WP
@@ -246,7 +246,7 @@ end
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int.
let a1 = Load_S1_S a t t2 t1 in
let a2 = Load_S1_S a t (set t2 (shiftfield_F1_S_f a) i) t1 in
- region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
+ region (a.base) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
end
[wp] 1 goal generated
------------------------------------------------------------
--
GitLab