blob: b9f7bd7551837318151bb0b3a1f8b72a44695d66 (
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;
|