Dafny: automatically update iterator _new field upon allocations

2 files changed, 38 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index df0451d5..4de9e965 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1639,6 +1639,10 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Then

     (0,0): anon3

+Iterators.dfy(174,28): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon15_Then

 Iterators.dfy(37,14): Error BP5002: A precondition for this call might not hold.

 Iterators.dfy(1,10): Related location: This is the precondition that might not hold.

 Execution trace:

@@ -1666,7 +1670,7 @@ Execution trace:
     (0,0): anon4_Then

     (0,0): anon3

 

-Dafny program verifier finished with 27 verified, 7 errors

+Dafny program verifier finished with 34 verified, 8 errors

 

 -------------------- Superposition.dfy --------------------

 

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index e1461622..2473daa0 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -117,7 +117,7 @@ method TestIterB()
   }

 }

 

-// -----------------------------------------------------------

+// ------------------ yield statements, and_decreases variables ----------------------------------

 

 iterator IterC(c: Cell)

   requires c != null;

@@ -152,3 +152,35 @@ method TestIterC()
   more := iter.MoveNext();  // error: iter.Valid() may not hold

 }

 

+// ------------------ allocations inside an iterator ------------------

+

+iterator AllocationIterator(x: Cell)

+{

+  assert _new == {};

+  var h := new Cell;

+  assert _new == {h};

+

+  SomeMethod();

+  assert x !in _new;

+  assert null !in _new;

+  assert h in _new;

+

+  ghost var saveNew := _new;

+  var u, v := AnotherMethod();

+  assert u in _new;

+  if {

+    case true =>  assert v in _new - saveNew ==> v != null && fresh(v);

+    case true =>  assert !fresh(v) ==> v !in _new;

+    case true =>  assert v in _new;  // error: it may be, but, then again, it may not be

+  }

+}

+

+static method SomeMethod()

+{

+}

+

+static method AnotherMethod() returns (u: Cell, v: Cell)

+  ensures u != null && fresh(u);

+{

+  u := new Cell;

+}