Dafny: good error locations for yield statements; other iterator improvements / bug fixes

1 files changed, 30 insertions, 0 deletions

diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index 64d1ebd3..60b1bc7e 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -106,3 +106,33 @@ module Mx {
     }

   }

 }

+

+// --------------------------------- _decreases<n> fields

+

+class Cell

+{

+  var data: int;

+}

+

+iterator Dieter0(c: Cell)

+  requires c != null;

+  decreases c.data, c.data, c != null;

+{

+  assert _decreases0 == _decreases1;

+  assert _decreases2;

+  assert _decreases3 == null;  // error: there is no _decreases3

+  assert _decreases0 == null;  // error: type mismatch

+  _decreases2 := false;  // error: the field is immutable

+}

+

+iterator Dieter1(c: Cell)

+  requires c != null;

+{

+  assert _decreases0 == c;

+  assert _decreases1;  // error: there is no _decreases1

+}

+

+iterator Dieter2()

+{

+  assert _decreases0 == null;  // error: there is no _decreases0

+}