blob: d2defb2580d887e04bdca345db51a5d3277cf50f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
// RUN: %boogie -noinfer %s > %t
// RUN: %diff %s.expect %t
// 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;
|