diff options
Diffstat (limited to 'Test/test20/PolyProcs0.bpl')
-rw-r--r-- | Test/test20/PolyProcs0.bpl | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl index 698e2f12..cc0ba491 100644 --- a/Test/test20/PolyProcs0.bpl +++ b/Test/test20/PolyProcs0.bpl @@ -1,35 +1,35 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-type Field a;
-
-function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
- returns (res:b);
-
-procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
- returns (res:b) {
- start:
- res := heap[f, obj]; // error: wrong argument order
- res := heap[obj, f];
- assert res == FieldAccessFun(heap, obj, f);
- return;
-}
-
-procedure UseHeap(heap : <a>[ref, Field a]a) {
- var f1 : Field int; var f2 : Field bool; var obj : ref;
- var x : int; var y : bool;
-
- call x := FieldAccess(heap, f1, obj); // error: wrong argument order
- call x := FieldAccess(heap, obj, f1);
- call y := FieldAccess(heap, obj, f2);
-
- call y := FieldAccess(heap, obj, f1); // error: wrong result type
- call x := FieldAccess(heap, obj, obj); // error: wrong argument type
-}
-
-procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b);
- requires obj0 != obj1;
- ensures heap[obj0, f] != heap[obj1, f];
-
-type ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +type Field a; + +function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b) + returns (res:b); + +procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b) + returns (res:b) { + start: + res := heap[f, obj]; // error: wrong argument order + res := heap[obj, f]; + assert res == FieldAccessFun(heap, obj, f); + return; +} + +procedure UseHeap(heap : <a>[ref, Field a]a) { + var f1 : Field int; var f2 : Field bool; var obj : ref; + var x : int; var y : bool; + + call x := FieldAccess(heap, f1, obj); // error: wrong argument order + call x := FieldAccess(heap, obj, f1); + call y := FieldAccess(heap, obj, f2); + + call y := FieldAccess(heap, obj, f1); // error: wrong result type + call x := FieldAccess(heap, obj, obj); // error: wrong argument type +} + +procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b); + requires obj0 != obj1; + ensures heap[obj0, f] != heap[obj1, f]; + +type ref; |