blob: 5828b0bf939d94759ae6cab349e825099cfeaca3 (
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
|
class Test {
var x: int
var tk: token<Test.incX>
predicate V { acc(x) }
method incX()
requires V
ensures V
{
unfold V
x := x + 1
fold V
}
method joinTk()
requires acc(tk) && tk != null && acc(tk.joinable) && tk.joinable
requires eval(tk.fork this.incX(), true)
ensures V
ensures unfolding V in x == old(x) // ERROR: old(x) is not readable (no error here, previously)
{
join tk
assert V
}
method test()
requires acc(x) && x == 0
requires acc(tk)
{
fold V
fork tklocal := incX()
tk := tklocal
call joinTk()
unfold V
assert x == old(x) // this verified previously (without any errors anywhere in the file)
}
}
|
