Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequences

1 files changed, 14 insertions, 1 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a5f02dc6..7cbabcd7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -309,7 +309,7 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
   }

 }

 

-// ----------------------- tests that involve sequences of boxed booleans --------

+// ----------------------- tests that involve sequences of boxes --------

 

 ghost method M(zeros: seq<bool>, Z: bool)

   requires 1 <= |zeros| && Z == false;

@@ -318,3 +318,16 @@ ghost method M(zeros: seq<bool>, Z: bool)
   var x := [Z];

   assert zeros[0..1] == [Z];

 }

+

+class SomeType

+{

+  var x: int;

+  method DoIt(stack: seq<SomeType>)

+    modifies stack;

+  {

+    // the following line once gave rise to a crash in the translation

+    foreach (n in stack) {

+      n.x := 10;

+    }

+  }

+}