blob: 15072d416c0742041ef331852ec5a602abfd7347 (
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
|
class Test {
var x: int;
method m(a:int) returns (b:int)
{
var c := 0;
ghost const d,c [d == c];
var b [b == 0];
var e [e == a];
assert d == c;
assert e == a;
assert b == 0;
assert c == 0; // error
}
method n()
requires acc(x);
{
x := 0;
const y [acc(x), rd(x) && x == old(x) + 1 && y == x];
assert y == 1;
const v [rd(x), rd(x) && v == old(x) + 1];
assert v == 2;
const z [z == 1];
ghost var t [z == 1, true];
assert false; // reachable
}
method o()
{
var z [acc(x) && z == 0]; // unimplementable
x := z;
assert x == 0;
assert false; // reachable
}
}
|