Fixed problem with propagating allocation information about array elements.

Improved situation with (reducing bogosity of) type checking of "object".

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index d8bffce4..4cd06e53 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -253,3 +253,24 @@ method Test_ArrayElementLhsOfCall(a: array<int>, i: int, c: Cdefg<int>) returns
 class Cdefg<T> {

   var t: T;

 }

+

+// ---------- allocation business -----------

+

+class MyClass {

+  ghost var Repr: set<object>;

+}

+

+method AllocationBusinessA(a: array<MyClass>, j: int)

+  requires a != null && 0 <= j < a.Length;

+  requires a[j] != null;

+{

+  var c := new MyClass;

+  assert c !in a[j].Repr;  // the proof requires allocation axioms for arrays

+}

+method AllocationBusinessB(a: array2<MyClass>, i: int, j: int)

+  requires a != null && 0 <= i < a.Length0 && 0 <= j < a.Length1;

+  requires a[i,j] != null;

+{

+  var c := new MyClass;

+  assert c !in a[i,j].Repr;  // the proof requires allocation axioms for multi-dim arrays

+}