Chalice/tests/regressions/workitem-8234.chalice


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

class Test{
	var tests : seq<Test>;
	var total : int;
	
	invariant acc(tests, 100);
	invariant acc(total, 50);
	
	function at(loc : int) : Test
		requires acc(tests);
		requires loc >= 0 && loc < size();
	{
		tests[loc]
	}
	
	
	function size() : int
		requires acc(tests);
		ensures result >= 0;
		ensures result == |tests|; // previously, there was a nullpointer exception here
	{
		|tests|
	}
	
	predicate pre
	{ acc(total, 50) }
}