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;