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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type T;
var Heap: <x>[ref,Field x]x;
function IsHeap(<x>[ref,Field x]x) returns (bool);
const alloc: Field bool;
const C.x: Field int;
axiom (forall h: <x>[ref,Field x]x, f: Field ref, o: ref :: IsHeap(h) && o != null ==> h[h[o,f], alloc]);
procedure P(this: ref) returns (r: int)
modifies Heap;
{
start:
r := Heap[this, C.x];
Heap[this, C.x] := r;
return;
}
// -----------------
procedure R(this: ref)
modifies Heap;
{
var field: any, refField: Field ref, yField: Field y, anyField: Field any;
var b: bool, a: any;
start:
b := Heap[this, C.x]; // type error
Heap[this, C.x] := true; // type error
Heap[this, refField] := this;
Heap[this, yField] := 2; // type error
Heap[this, field] := a; // type error
Heap[this, field] := b; // type error
Heap[this, anyField] := a;
Heap[this, anyField] := b;
Heap[this, anyField] := anyField;
Heap[this, anyField] := yField;
Heap[this, anyField] := field;
return;
}
type Field a;
type y;
type ref, any;
const null : ref;
|
