Chalice/tests/regressions/workitem-8236.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

class Bug{

	method Main() // expected ERROR: method might lock/unlock more than allowed
	{
		var a : Bug;
		call a:= m();
	}

	method m() returns (a : Bug)
		lockchange a // resulted previously in Boogie errors
	{
		a := new Bug;
		share a;
		acquire a;
	}
}