Commit 08b3a7ae authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Test: check that array defs are not shared

parent f38cca53
/* run.config
OPT:-wp-gen -wp-prover=why3 -wp-msg-key=print-generated
*/
/* run.config_qualif
DONTRUN:
*/
struct S { int f ; unsigned a[5] ; long b[5] ; };
/*@ ensures *p == \old(*p) ; */
void job(struct S *p, int v)
{
p->f = v;
}
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/multi_matrix_types.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
---------------------------------------------
--- Context 'typed_job' Cluster 'Matrix'
---------------------------------------------
theory Matrix
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.cint.Cint *)
predicate IsArray_uint32 (t:int -> int) = forall i:int. is_uint32 (get t i)
predicate IsArray_sint32 (t:int -> int) = forall i:int. is_sint32 (get t i)
predicate EqArray_int (n:int) (t:int -> int) (t1:int -> int) =
forall i:int. 0 <= i -> i < n -> get t1 i = get t i
end
---------------------------------------------
--- Context 'typed_job' Cluster 'S1_S'
---------------------------------------------
theory S1_S
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
type S1_S =
| S1_S1 (F1_S_a:int -> int) (F1_S_b:int -> int) (F1_S_f:int)
(* use Matrix *)
predicate IsS1_S (s:S1_S) =
(IsArray_sint32 (F1_S_b s) /\ IsArray_uint32 (F1_S_a s)) /\
is_sint32 (F1_S_f s)
predicate EqS1_S (s:S1_S) (s1:S1_S) =
(F1_S_f s1 = F1_S_f s /\ EqArray_int 5 (F1_S_a s) (F1_S_a s1)) /\
EqArray_int 5 (F1_S_b s) (F1_S_b s1)
end
---------------------------------------------
--- Context 'typed_job' Cluster 'Compound'
---------------------------------------------
theory Compound
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
function shiftfield_F1_S_f (p:addr) : addr = shift p 0
function shiftfield_F1_S_a (p:addr) : addr = shift p 1
function shift_uint32 (p:addr) (k:int) : addr = shift p k
function Array_uint32 addr int (addr -> int) : int -> int
function shiftfield_F1_S_b (p:addr) : addr = shift p 6
function shift_sint32 (p:addr) (k:int) : addr = shift p k
function Array_sint32 addr int (addr -> int) : int -> int
(* use S1_S *)
function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) : S1_S =
S1_S1 (Array_uint32 (shiftfield_F1_S_a p) 5 mint)
(Array_sint32 (shiftfield_F1_S_b p) 5 mint1)
(get mint1 (shiftfield_F1_S_f p))
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 :
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 :
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 :
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_sint32_access :
forall mint:addr -> int, i:int, n:int, p:addr
[get (Array_sint32 p n mint) i].
0 <= i ->
i < n -> get (Array_sint32 p n mint) i = get mint (shift_sint32 p i)
Q_Array_sint32_update_Mint0 :
forall mint:addr -> int, n:int, p:addr, q:addr, v:int
[Array_sint32 p n (set mint q v)].
not q = p -> Array_sint32 p n (set mint q v) = Array_sint32 p n mint
Q_Array_sint32_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint32 p n mint, eqmem mint mint1 q n1| Array_sint32 p n mint1,
eqmem mint mint1 q n1].
included p 1 q n1 ->
eqmem mint mint1 q n1 -> Array_sint32 p n mint1 = Array_sint32 p n mint
Q_Array_sint32_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
[Array_sint32 p n (havoc mint1 mint q n1)].
separated p 1 q n1 ->
Array_sint32 p n (havoc mint1 mint q n1) = Array_sint32 p n mint
Q_Load_S1_S_update_Mint0 :
forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
[Load_S1_S p (set mint q v) mint1].
separated p 11 q 1 ->
Load_S1_S p (set mint q v) mint1 = Load_S1_S p mint mint1
Q_Load_S1_S_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
addr, q:addr [Load_S1_S p mint mint2, eqmem mint mint1 q n|
Load_S1_S p mint1 mint2, eqmem mint mint1 q n].
included p 11 q n ->
eqmem mint mint1 q n -> Load_S1_S p mint1 mint2 = Load_S1_S p mint mint2
Q_Load_S1_S_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
addr, q:addr [Load_S1_S p (havoc mint1 mint q n) mint2].
separated p 11 q n ->
Load_S1_S p (havoc mint1 mint q n) mint2 = Load_S1_S p mint mint2
Q_Load_S1_S_update_Mint1 :
forall mint:addr -> int, mint1:addr -> int, p:addr, q:addr, v:int
[Load_S1_S p mint1 (set mint q v)].
separated p 11 q 1 ->
Load_S1_S p mint1 (set mint q v) = Load_S1_S p mint1 mint
Q_Load_S1_S_eqmem_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
addr, q:addr [Load_S1_S p mint2 mint, eqmem mint mint1 q n|
Load_S1_S p mint2 mint1, eqmem mint mint1 q n].
included p 11 q n ->
eqmem mint mint1 q n -> Load_S1_S p mint2 mint1 = Load_S1_S p mint2 mint
Q_Load_S1_S_havoc_Mint1 :
forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, n:int, p:
addr, q:addr [Load_S1_S p mint2 (havoc mint1 mint q n)].
separated p 11 q n ->
Load_S1_S p mint2 (havoc mint1 mint q n) = Load_S1_S p mint2 mint
end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
(* use S1_S *)
(* use Compound *)
goal wp_goal :
forall t:addr -> int, t1:addr -> int, a:addr, i:int.
let a1 = Load_S1_S a t t1 in
let a2 = Load_S1_S a t (set t1 (shiftfield_F1_S_f a) i) in
region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
end
[wp] 1 goal generated
------------------------------------------------------------
Function job
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/multi_matrix_types.i, line 10) in 'job':
Let a = Load_S1_S(p, Mint_0, Mint_1).
Let a_1 = Load_S1_S(p, Mint_0, Mint_1[shiftfield_F1_S_f(p) <- v]).
Assume {
Type: IsS1_S(a) /\ IsS1_S(a_1).
(* Heap *)
Type: region(p.base) <= 0.
}
Prove: EqS1_S(a_1, a).
------------------------------------------------------------
Markdown is supported
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