diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test20/PolyProcs0.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test20/PolyProcs0.bpl')
| -rw-r--r-- | Test/test20/PolyProcs0.bpl | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl new file mode 100644 index 00000000..609f1167 --- /dev/null +++ b/Test/test20/PolyProcs0.bpl @@ -0,0 +1,44 @@ +
+
+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];
+
+procedure testCallForall(heap : <a>[ref, Field a]a) {
+ var f1 : Field int; var f2 : Field bool;
+
+ start:
+ call forall injective(heap, *, *, f1);
+ call forall injective(heap, *, *, f2);
+ call forall injective(heap, *, *, *);
+
+ call forall injective(heap, *, f1, *); // error: wrong argument type
+}
+
+type ref;
|