diff options
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
-rw-r--r-- | Test/dafny0/SmallTests.dfy | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index b4dc6599..ac7286e9 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -308,7 +308,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;
@@ -317,3 +317,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;
+ }
+ }
+}
|