From 4977e01decc2823eda691acea9bbbe7e537c14dc Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Tue, 12 Jun 2012 13:53:03 -0700
Subject: Dafny: beefed up allocation axioms for boxes stored in fields

---
 Binaries/DafnyPrelude.bpl |  5 +++++
 Test/dafny2/Answer        |  4 ++++
 Test/dafny2/TreeFill.dfy  | 27 +++++++++++++++++++++++++++
 Test/dafny2/runtest.bat   |  2 +-
 4 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny2/TreeFill.dfy

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 742fd4e4..fef8fe1f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -558,6 +558,11 @@ axiom (forall x: int, h: HeapType ::
 axiom (forall r: ref, h: HeapType ::
   { GenericAlloc($Box(r), h) }
   $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));
+// boxes in the heap
+axiom (forall r: ref, f: Field BoxType, h: HeapType ::
+  { GenericAlloc(read(h, r, f), h) }
+  $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
+  GenericAlloc(read(h, r, f), h));
 
 // ---------------------------------------------------------------
 // -- Arrays -----------------------------------------------------
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 9f7fad4e..b0bbfe05 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -31,6 +31,10 @@ Dafny program verifier finished with 23 verified, 0 errors
 
 Dafny program verifier finished with 5 verified, 0 errors
 
+-------------------- TreeFill.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
 -------------------- StoreAndRetrieve.dfy --------------------
 
 Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
new file mode 100644
index 00000000..f7e2cc89
--- /dev/null
+++ b/Test/dafny2/TreeFill.dfy
@@ -0,0 +1,27 @@
+datatype Tree<T> = Null | Node(Tree, T, Tree);
+
+function Contains<T>(t: Tree, v: T): bool
+{
+  match t
+  case Null => false
+  case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)
+}
+
+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
+  requires a != null && 0 <= start <= a.Length;
+  modifies a;
+  ensures start <= end <= a.Length;
+  ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);
+  ensures forall i :: start <= i < end ==> Contains(t, a[i]);
+{
+  match (t) {
+    case Null =>
+      end := start;
+    case Node(left, x, right) =>
+      end := Fill(left, a, start);
+      if (end < a.Length) {
+        a[end] := x;
+        end := Fill(right, a, end + 1);
+      }
+  }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 494a8721..794b7908 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -14,7 +14,7 @@ for %%f in (
     COST-verif-comp-2011-2-MaxTree-datatype.dfy
     COST-verif-comp-2011-3-TwoDuplicates.dfy
     COST-verif-comp-2011-4-FloydCycleDetect.dfy
-    Intervals.dfy
+    Intervals.dfy TreeFill.dfy
     StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy
   ) do (
   echo.
-- 
cgit v1.2.3