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

3 files changed, 79 insertions, 8 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 358a64bf..df0451d5 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1623,18 +1623,50 @@ IteratorResolution.dfy(79,13): Error: when allocating an object of type 'Generic
 IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)

 IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field

 IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field

-7 resolution/type errors detected in IteratorResolution.dfy

+IteratorResolution.dfy(123,9): Error: unresolved identifier: _decreases3

+IteratorResolution.dfy(124,21): Error: arguments must have the same type (got int and ?)

+IteratorResolution.dfy(125,14): Error: LHS of assignment does not denote a mutable field

+IteratorResolution.dfy(132,9): Error: unresolved identifier: _decreases1

+IteratorResolution.dfy(137,9): Error: unresolved identifier: _decreases0

+12 resolution/type errors detected in IteratorResolution.dfy

 

 -------------------- Iterators.dfy --------------------

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

+Iterators.dfy(100,22): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Iterators.dfy(103,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

+    (0,0): anon3

+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:

     (0,0): anon0

-    (0,0): anon31_Then

+    (0,0): anon37_Then

+    (0,0): anon2

+    (0,0): anon38_Then

+    (0,0): anon5

+    (0,0): anon39_Then

+Iterators.dfy(86,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Iterators.dfy(116,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Iterators.dfy(147,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+Iterators.dfy(152,16): Error BP5002: A precondition for this call might not hold.

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Then

     (0,0): anon3

-    (0,0): anon32_Then

 

-Dafny program verifier finished with 16 verified, 1 error

+Dafny program verifier finished with 27 verified, 7 errors

 

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

 

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

+}

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 36ba94cb..e1461622 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -93,9 +93,14 @@ iterator IterB(c: Cell)
   modifies c;

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

   ensures true;

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

 {

+  assert _decreases0 == c;

+  assert _decreases1 == (c != null);

+  assert _decreases2 == c.data;  // error: c is not protected by the reads clause

+  var tmp := c.data;

   if (*) { yield; }

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

+  assert tmp == c.data;  // error: c is not protected by the reads clause

   c.data := *;

 }

 

@@ -120,9 +125,13 @@ iterator IterC(c: Cell)
   reads c;

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

   ensures true;

+  decreases c, c, c.data;

 {

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

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

+  assert _decreases2 == c.data;  // this time, all is fine, because the iterator has an appropriate reads clause

+  var tmp := c.data;

+  if (*) { yield; }

+  if (*) { yield; }

+  assert tmp == c.data;  // this time, all is fine, because the iterator has an appropriate reads clause

   c.data := *;

 }