diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 19:17:07 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 19:17:07 -0700 |
| commit | c624c990202819ee6789f4d56acbe716680071c0 (patch) | |
| tree | 12ef511c162cd7ef3efedef25a063759564e50e6 /Test | |
| parent | 8b6912828c27c267fc5ce17945d19ccc217d1201 (diff) | |
| parent | 126bbea00d28c22f4ac21c773e7790ad9015e82f (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 15 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 13 |
4 files changed, 29 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1a3218eb..05250fa8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -201,7 +201,7 @@ Execution trace: (0,0): anon15
(0,0): anon25_Else
-Dafny program verifier finished with 41 verified, 14 errors
+Dafny program verifier finished with 43 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
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;
+ }
+ }
+}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 0111f9af..5ee9f921 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -81,7 +81,7 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 29 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index de5a3358..15cc1ffe 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -153,6 +153,19 @@ class DatatypeInduction<T> { }
// see also Test/dafny0/DTypes.dfy for more variations of this example
+
+ function OccurrenceCount<T>(tree: Tree<T>, x: T): int
+ {
+ match tree
+ case Leaf(t) => if x == t then 1 else 0
+ case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
+ }
+ method RegressionTest(tree: Tree<T>)
+ // the translation of the following line once crashed Dafny
+ requires forall y :: 0 <= OccurrenceCount(tree, y);
+ {
+ }
+
}
// ----------------------- Induction and case splits -----------------
|