blob: 342c5b19b1fbee097bf2532c7cee37f470b70f75 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
// Test old appearing in illegal locations
var Global0: int;
// Bad
procedure OldInCode1()
requires old(Global0) == 0;
{
start:
return;
}
// Bad
axiom (forall o:ref :: old(o) == o);
type ref;
|