blob: 201b643db43203db65205037906f11cc6c91f06a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
class Cell
{
var value:int;
predicate P { acc(value,50) }
function get():int
requires P;
{
unfolding P in value
}
method boom(x:Cell, y:Cell)
requires x!=null && y!=null && x.P && y.P;
ensures x.P && y.P && (x==y ==> x.get()==100) && (x!=y ==> x.get()==old(x.get()));
{
if(x==y)
{
unfold x.P; unfold x.P;
y.value:=100;
fold y.P; fold y.P;
}
}
method skip()
requires P;
ensures P;
{}
// is the bookkeeping correct when calculating the secondary mask?
// fold happens once on a statically unknown object
// intermediate calls to skip happen in all examples to create artificial "changes" to the heap,
// thereby testing framing in the bookkeeping of folds/unfolds
method foo(z:Cell)
requires acc(value,50) && value==2 && z!=null && acc(z.value,50);
{
fold z.P;
call z.skip();
fold P;
call boom(this, z);
assert this!=z ==> unfolding P in value==2;
assert this==z ==> unfolding P in value==100;
}
// must fail: give away all permission, even in pieces, and you lose all information about value
method hoo()
requires acc(value);
{
fold P;
call skip();
fold P;
fork t:=skip();
call skip ();
assert unfolding P in value==old(value); // ERROR: should fail
}
}
|
