Dafny: changed iterator body to resolve to implicit fields rather than to the formal in- and yield-parameters

1 files changed, 4 insertions, 2 deletions

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 680c2812..3f06e445 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -91,10 +91,11 @@ method TestIterA()
 iterator IterB(c: Cell)

   requires c != null;

   modifies c;

-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause

+  yield ensures c.data == old(c.data);

   ensures true;

 {

   if (*) { yield; }

+  if (*) { yield; }  // error: cannot prove the yield-ensures clause here (needs a reads clause)

   c.data := *;

 }

 

@@ -117,10 +118,11 @@ iterator IterC(c: Cell)
   requires c != null;

   modifies c;

   reads c;

-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause

+  yield ensures c.data == old(c.data);

   ensures true;

 {

   if (*) { yield; }

+  if (*) { yield; }  // this time, all is fine, because the iterator has an appropriate reads clause

   c.data := *;

 }