diff options
Diffstat (limited to 'Test/test1/Family.bpl')
-rw-r--r-- | Test/test1/Family.bpl | 98 |
1 files changed, 49 insertions, 49 deletions
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl index fec96332..0ec5fb20 100644 --- a/Test/test1/Family.bpl +++ b/Test/test1/Family.bpl @@ -1,49 +1,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;
+// 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; |