1 files changed, 47 insertions, 0 deletions
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl
new file mode 100644
index 00000000..1c650d3d
--- /dev/null
+++ b/Test/test1/Family.bpl
@@ -0,0 +1,47 @@
+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;