blob: fd51977dc84856e4a727ca6cceef758cba22f8dd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
class Cell { var x: int }
class Test {
method get() returns (c: Cell)
ensures c != null
lockchange c /* previosly, this introduced errors */
{
c := new Cell
}
/* method was needed to get Boogie errors */
method testRd() // expected ERROR: method might lock/unlock more than allowed
{
var x: Cell
call x := get()
}
}
|
