Skip to content
Snippets Groups Projects
Commit ce445a3d authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] tests oracles related to Why3 VC format

parent 353848e4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 96 additions and 95 deletions
src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+ 1
− 1
View file @ ce445a3d
...@@ -57,7 +57,7 @@ end ...@@ -57,7 +57,7 @@ end
let m3 = set m2 (shift_sint32 a 3) (get m2 a2) in let m3 = set m2 (shift_sint32 a 3) (get m2 a2) in
0 <= i1 -> 0 <= i1 ->
0 <= i -> 0 <= i ->
region (base a) <= 0 -> region (a.base) <= 0 ->
i1 <= 9 -> i1 <= 9 ->
i <= 9 -> i <= 9 ->
linked t -> linked t ->
......
src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+ 11
− 11
View file @ ce445a3d
...@@ -75,13 +75,13 @@ theory A_Occ ...@@ -75,13 +75,13 @@ theory A_Occ
(* use Chunk *) (* use Chunk *)
Q_empty : axiom Q_empty :
forall mint:addr -> int, v:int, p:addr, f:int, t:int. 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 t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
(* use Compound *) (* use Compound *)
Q_is : axiom Q_is :
forall mint:addr -> int, v:int, p:addr, f:int, t:int. forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in let x1 = get mint (shift_sint32 p x) in
...@@ -91,7 +91,7 @@ theory A_Occ ...@@ -91,7 +91,7 @@ theory A_Occ
is_sint32 v -> is_sint32 v ->
is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t 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. forall mint:addr -> int, v:int, p:addr, f:int, t:int.
let x = (- 1) + t in let x = (- 1) + t in
let x1 = get mint (shift_sint32 p x) in let x1 = get mint (shift_sint32 p x) in
...@@ -154,7 +154,7 @@ end ...@@ -154,7 +154,7 @@ end
forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int. forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
i3 <= i1 -> i3 <= i1 ->
i < i3 -> i < i3 ->
region (base a) <= 0 -> region (a.base) <= 0 ->
is_sint32_chunk t -> is_sint32_chunk t ->
is_uint32 i3 -> is_uint32 i3 ->
is_uint32 i1 -> is_uint32 i1 ->
...@@ -233,14 +233,14 @@ theory A_Occ1 ...@@ -233,14 +233,14 @@ theory A_Occ1
(* use Chunk1 *) (* use Chunk1 *)
Q_empty1 : axiom Q_empty1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int. forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
t <=' f -> t <=' f ->
is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0 is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
(* use Compound1 *) (* use Compound1 *)
Q_is1 : axiom Q_is1 :
forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int. forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in let x1 = get1 mint (shift_sint321 p x) in
...@@ -250,7 +250,7 @@ theory A_Occ1 ...@@ -250,7 +250,7 @@ theory A_Occ1
is_sint321 v -> is_sint321 v ->
is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t 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. forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
let x = (- 1) +' t in let x = (- 1) +' t in
let x1 = get1 mint (shift_sint321 p x) in let x1 = get1 mint (shift_sint321 p x) in
...@@ -315,7 +315,7 @@ end ...@@ -315,7 +315,7 @@ end
let x = (- 1) +' i1 in let x = (- 1) +' i1 in
not get1 t (shift_sint321 a x) = i2 -> not get1 t (shift_sint321 a x) = i2 ->
i <' i1 -> i <' i1 ->
region1 (base1 a) <=' 0 -> region1 (a.base1) <=' 0 ->
i1 <=' 1000 -> i1 <=' 1000 ->
is_sint32_chunk1 t -> is_sint32_chunk1 t ->
is_uint321 i1 -> is_uint321 i1 ->
...@@ -392,14 +392,14 @@ theory A_Occ2 ...@@ -392,14 +392,14 @@ theory A_Occ2
(* use Chunk2 *) (* use Chunk2 *)
Q_empty2 : axiom Q_empty2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int. forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
t <='' f -> t <='' f ->
is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0 is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
(* use Compound2 *) (* use Compound2 *)
Q_is2 : axiom Q_is2 :
forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int. forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in let x1 = get2 mint (shift_sint322 p x) in
...@@ -409,7 +409,7 @@ theory A_Occ2 ...@@ -409,7 +409,7 @@ theory A_Occ2
is_sint322 v -> is_sint322 v ->
is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t 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. forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
let x = (- 1) +'' t in let x = (- 1) +'' t in
let x1 = get2 mint (shift_sint322 p x) in let x1 = get2 mint (shift_sint322 p x) in
......
src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+ 15
− 15
View file @ ce445a3d
...@@ -138,42 +138,42 @@ end ...@@ -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 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: 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. forall i:int.
begin <= i -> begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b 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) 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 i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\ get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
begin <= i) /\ begin1 <= i) /\
i < j) /\ i < j) /\
j < end1) /\ j < end1) /\
(forall i1:int. (forall i1:int.
not i1 = i -> not i1 = i ->
not j = i1 -> not j = i1 ->
begin <= i1 -> begin1 <= i1 ->
i1 < end1 -> i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1)) get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int = inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl : | 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. int, end1:int.
P_same_array mint mint1 a b begin end1 -> P_same_array mint mint1 a b begin1 end1 ->
P_same_elements mint mint1 a b begin end1 P_same_elements mint mint1 a b begin1 end1
| Q_swap : | 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. int, i:int, j:int, end1:int.
P_swap mint mint1 a b begin i j end1 -> P_swap mint mint1 a b begin1 i j end1 ->
P_same_elements mint mint1 a b begin end1 P_same_elements mint mint1 a b begin1 end1
| Q_trans : | Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a: forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
addr, b:addr, c:addr, begin:int, end1:int. addr, b:addr, c:addr, begin1:int, end1:int.
P_same_elements mint mint1 b c begin end1 -> P_same_elements mint mint1 b c begin1 end1 ->
P_same_elements mint1 mint2 a b begin end1 -> P_same_elements mint1 mint2 a b begin1 end1 ->
P_same_elements mint mint2 a c begin end1 P_same_elements mint mint2 a c begin1 end1
goal wp_goal : goal wp_goal :
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i: forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
......
src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
+ 3
− 2
View file @ ce445a3d
...@@ -22,13 +22,14 @@ ...@@ -22,13 +22,14 @@
predicate P_RP int 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_F (i:int) : int = 2 * i
function L_RF int : int 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)) 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) goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
......
src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+ 20
− 20
View file @ ce445a3d
...@@ -89,13 +89,13 @@ theory Compound ...@@ -89,13 +89,13 @@ theory Compound
Init_S1_X1 (get init (shiftfield_F1_X_a p)) Init_S1_X1 (get init (shiftfield_F1_X_a p))
(get init (shiftfield_F1_X_b p)) (get init (shiftfield_F1_X_c 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: 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]. addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
separated p 3 q 1 -> separated p 3 q 1 ->
Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1 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: 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, 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, eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
...@@ -104,21 +104,21 @@ theory Compound ...@@ -104,21 +104,21 @@ theory Compound
eqmem mchar mchar1 q n -> eqmem mchar mchar1 q n ->
Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1 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: forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr addr -> int, n:int, p:addr, q:addr
[Load_S1_X p (havoc mchar1 mchar q n) mint mint1]. [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
separated p 3 q n -> separated p 3 q n ->
Load_S1_X p (havoc mchar1 mchar q n) mint mint1 Load_S1_X p (havoc mchar1 mchar q n) mint mint1 =
= Load_S1_X p mchar 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: 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]. addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
separated p 3 q 1 -> separated p 3 q 1 ->
Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint 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 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, -> 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, eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
...@@ -127,21 +127,21 @@ theory Compound ...@@ -127,21 +127,21 @@ theory Compound
eqmem mint1 mint2 q n -> eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint 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 forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr -> int, n:int, p:addr, q:addr
[Load_S1_X p mchar (havoc mint2 mint1 q n) mint]. [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
separated p 3 q n -> separated p 3 q n ->
Load_S1_X p mchar (havoc mint2 mint1 q n) mint Load_S1_X p mchar (havoc mint2 mint1 q n) mint =
= Load_S1_X p mchar mint1 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: 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)]. addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
separated p 3 q 1 -> separated p 3 q 1 ->
Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1 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 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, -> 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, eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
...@@ -150,28 +150,28 @@ theory Compound ...@@ -150,28 +150,28 @@ theory Compound
eqmem mint1 mint2 q n -> eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1 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 forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr -> int, n:int, p:addr, q:addr
[Load_S1_X p mchar mint (havoc mint2 mint1 q n)]. [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
separated p 3 q n -> separated p 3 q n ->
Load_S1_X p mchar mint (havoc mint2 mint1 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 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 forall init:addr -> bool, p:addr, q:addr, v:bool
[Load_Init_S1_X p (set init q v)]. [Load_Init_S1_X p (set init q v)].
separated p 3 q 1 -> separated p 3 q 1 ->
Load_Init_S1_X p (set init q v) = Load_Init_S1_X p init 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 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, [Load_Init_S1_X p init, eqmem init init1 q n| Load_Init_S1_X p init1,
eqmem init init1 q n]. eqmem init init1 q n].
included p 3 q n -> included p 3 q n ->
eqmem init init1 q n -> Load_Init_S1_X p init1 = Load_Init_S1_X p init 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 forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
[Load_Init_S1_X p (havoc init1 init q n)]. [Load_Init_S1_X p (havoc init1 init q n)].
separated p 3 q n -> separated p 3 q n ->
...@@ -236,7 +236,7 @@ end ...@@ -236,7 +236,7 @@ end
forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3: forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3:
addr -> int, t4:addr -> int, a:addr. addr -> int, t4:addr -> int, a:addr.
Load_Init_S1_X a t = x -> Load_Init_S1_X a t = x ->
region (base a) <= 0 -> region (a.base) <= 0 ->
is_sint16_chunk t3 -> is_sint16_chunk t3 ->
is_sint32_chunk t4 -> is_sint32_chunk t4 ->
is_sint8_chunk t2 -> is_sint8_chunk t2 ->
...@@ -272,7 +272,7 @@ end ...@@ -272,7 +272,7 @@ end
goal wp_goal : goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4: forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
addr -> int, a:addr, x:S1_X. addr -> int, a:addr, x:S1_X.
region (base a) <= 0 -> region (a.base) <= 0 ->
IsS1_X x -> IsS1_X x ->
is_sint16_chunk t3 -> is_sint16_chunk t3 ->
is_sint32_chunk t4 -> is_sint32_chunk t4 ->
......
src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+ 5
− 5
View file @ ce445a3d
...@@ -59,19 +59,19 @@ theory Compound ...@@ -59,19 +59,19 @@ theory Compound
function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0 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 forall mint:addr -> int, p:addr, q:addr, v:int
[Load_S2_A p (set mint q v)]. [Load_S2_A p (set mint q v)].
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint 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 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, [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
eqmem mint mint1 q n]. eqmem mint mint1 q n].
included p 1 q n -> included p 1 q n ->
eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint 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 forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p (havoc mint1 mint q n)]. [Load_S2_A p (havoc mint1 mint q n)].
separated p 1 q n -> separated p 1 q n ->
...@@ -104,8 +104,8 @@ end ...@@ -104,8 +104,8 @@ end
let a3 = Load_S2_A a t in let a3 = Load_S2_A a t in
let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
not x = i -> not x = i ->
region (base a1) <= 0 -> region (a1.base) <= 0 ->
region (base a) <= 0 -> region (a.base) <= 0 ->
is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3 is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3
end end
[wp] 1 goal generated [wp] 1 goal generated
src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+ 15
− 15
View file @ ce445a3d
...@@ -101,42 +101,42 @@ end ...@@ -101,42 +101,42 @@ end
P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node 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: 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. forall i:int.
begin <= i -> begin1 <= i ->
i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b 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) 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 i) = get mint (shift_sint32 b j) /\
get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\ get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
begin <= i) /\ begin1 <= i) /\
i < j) /\ i < j) /\
j < end1) /\ j < end1) /\
(forall i1:int. (forall i1:int.
not i1 = i -> not i1 = i ->
not j = i1 -> not j = i1 ->
begin <= i1 -> begin1 <= i1 ->
i1 < end1 -> i1 < end1 ->
get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1)) get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
inductive P_same_elements (addr -> int) (addr -> int) addr addr int int = inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
| Q_refl : | 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. int, end1:int.
P_same_array mint mint1 a b begin end1 -> P_same_array mint mint1 a b begin1 end1 ->
P_same_elements mint mint1 a b begin end1 P_same_elements mint mint1 a b begin1 end1
| Q_swap : | 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. int, i:int, j:int, end1:int.
P_swap mint mint1 a b begin i j end1 -> P_swap mint mint1 a b begin1 i j end1 ->
P_same_elements mint mint1 a b begin end1 P_same_elements mint mint1 a b begin1 end1
| Q_trans : | Q_trans :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a: forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
addr, b:addr, c:addr, begin:int, end1:int. addr, b:addr, c:addr, begin1:int, end1:int.
P_same_elements mint mint1 b c begin end1 -> P_same_elements mint mint1 b c begin1 end1 ->
P_same_elements mint1 mint2 a b begin end1 -> P_same_elements mint1 mint2 a b begin1 end1 ->
P_same_elements mint mint2 a c begin end1 P_same_elements mint mint2 a c begin1 end1
goal wp_goal : goal wp_goal :
forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2: forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2:
......
src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+ 2
− 2
View file @ ce445a3d
...@@ -74,7 +74,7 @@ end ...@@ -74,7 +74,7 @@ end
goal wp_goal : goal wp_goal :
forall t:addr -> int, i:int, a:addr. forall t:addr -> int, i:int, a:addr.
let x = get t (shift_sint32 a i) in 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 end
[wp] 1 goal generated [wp] 1 goal generated
------------------------------------------------------------ ------------------------------------------------------------
...@@ -162,7 +162,7 @@ end ...@@ -162,7 +162,7 @@ end
goal wp_goal : goal wp_goal :
forall t:addr1 -> int, i:int, a:addr1. forall t:addr1 -> int, i:int, a:addr1.
let x = get1 t (shift_sint321 a i) in 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 end
[wp] 1 goal generated [wp] 1 goal generated
------------------------------------------------------------ ------------------------------------------------------------
......
src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+ 24
− 24
View file @ ce445a3d
...@@ -103,61 +103,61 @@ theory Compound ...@@ -103,61 +103,61 @@ theory Compound
(Array_uint32 (shiftfield_F1_S_a p) 5 mint) (Array_uint32 (shiftfield_F1_S_a p) 5 mint)
(Array_sint64 (shiftfield_F1_S_b p) 5 mint2) (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 forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_uint32 p n mint) i]. [get (Array_uint32 p n mint) i].
0 <= i -> 0 <= i ->
i < n -> get (Array_uint32 p n mint) i = get mint (shift_uint32 p 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 forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_uint32 p n (set mint q v)]. [Array_uint32 p n (set mint q v)].
not q = p -> Array_uint32 p n (set mint q v) = Array_uint32 p n mint 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 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, [Array_uint32 p n mint, eqmem mint mint1 q n1| Array_uint32 p n mint1,
eqmem mint mint1 q n1]. eqmem mint mint1 q n1].
included p 1 q n1 -> included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_uint32 p n mint1 = Array_uint32 p n mint 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 forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_uint32 p n (havoc mint1 mint q n1)]. [Array_uint32 p n (havoc mint1 mint q n1)].
separated p 1 q n1 -> separated p 1 q n1 ->
Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint 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 forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_sint64 p n mint) i]. [get (Array_sint64 p n mint) i].
0 <= i -> 0 <= i ->
i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p 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 forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_sint64 p n (set mint q v)]. [Array_sint64 p n (set mint q v)].
not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint 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 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, [Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
eqmem mint mint1 q n1]. eqmem mint mint1 q n1].
included p 1 q n1 -> included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint 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 forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint64 p n (havoc mint1 mint q n1)]. [Array_sint64 p n (havoc mint1 mint q n1)].
separated p 1 q n1 -> separated p 1 q n1 ->
Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint 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: 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]. addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
separated p 11 q 1 -> separated p 11 q 1 ->
Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2 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 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, -> 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, eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
...@@ -166,21 +166,21 @@ theory Compound ...@@ -166,21 +166,21 @@ theory Compound
eqmem mint mint1 q n -> eqmem mint mint1 q n ->
Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3 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 forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr -> int, n:int, p:addr, q:addr
[Load_S1_S p (havoc mint1 mint q n) mint2 mint3]. [Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
separated p 11 q n -> separated p 11 q n ->
Load_S1_S p (havoc mint1 mint q n) mint2 mint3 Load_S1_S p (havoc mint1 mint q n) mint2 mint3 =
= Load_S1_S p mint 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: 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]. addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
separated p 11 q 1 -> separated p 11 q 1 ->
Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint 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 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, -> 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, eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
...@@ -189,21 +189,21 @@ theory Compound ...@@ -189,21 +189,21 @@ theory Compound
eqmem mint1 mint2 q n -> eqmem mint1 mint2 q n ->
Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint 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 forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr -> int, n:int, p:addr, q:addr
[Load_S1_S p mint3 (havoc mint2 mint1 q n) mint]. [Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
separated p 11 q n -> separated p 11 q n ->
Load_S1_S p mint3 (havoc mint2 mint1 q n) mint Load_S1_S p mint3 (havoc mint2 mint1 q n) mint =
= Load_S1_S p mint3 mint1 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: 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)]. addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
separated p 11 q 1 -> separated p 11 q 1 ->
Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2 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 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, -> 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, eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
...@@ -212,13 +212,13 @@ theory Compound ...@@ -212,13 +212,13 @@ theory Compound
eqmem mint2 mint3 q n -> eqmem mint2 mint3 q n ->
Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2 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 forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
-> int, n:int, p:addr, q:addr -> int, n:int, p:addr, q:addr
[Load_S1_S p mint1 mint (havoc mint3 mint2 q n)]. [Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
separated p 11 q n -> separated p 11 q n ->
Load_S1_S p mint1 mint (havoc mint3 mint2 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 mint2
end end
[wp:print-generated] [wp:print-generated]
theory WP theory WP
...@@ -246,7 +246,7 @@ end ...@@ -246,7 +246,7 @@ end
forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int. 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 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 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 end
[wp] 1 goal generated [wp] 1 goal generated
------------------------------------------------------------ ------------------------------------------------------------
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment