diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:56:35 -0700 |
| commit | 0ef24f03ddd336f5efb5b7349d1957288a9343ef (patch) | |
| tree | 71015429f72da0c51aef1d5d0b57d18c10b5e97f /Test/dafny0 | |
| parent | 214218804b1cdc59113d4dcd7d6597942e5553e9 (diff) | |
Dafny: fixed regression tests
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 2 |
2 files changed, 12 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c2ecdcf4..35a5017b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -510,7 +510,7 @@ ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowe ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
-ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)
ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name
ResolutionErrors.dfy(55,7): Error: unresolved identifier: F
@@ -1557,6 +1557,16 @@ Execution trace: Dafny program verifier finished with 9 verified, 1 error
+-------------------- Maps.dfy --------------------
+Maps.dfy(76,8): Error: element may not be in domain
+Execution trace:
+ (0,0): anon0
+Maps.dfy(126,13): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 22 verified, 2 errors
+
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 0bc1004f..e74873e3 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -80,7 +80,7 @@ method test8(a: array<int>, i: int, j: int) method test9(a: array<int>, i: int, j: int, limit: int)
requires a != null && 0 <= i < j < limit <= a.Length;
modifies a;
- ensures old(multiset(a[0..limit])) == multiset(a[0..limit]);
+ ensures multiset(a[0..limit]) == old(multiset(a[0..limit]));
ensures a[j] == old (a[i]) && a[i] == old(a[j]);
ensures forall k :: 0 <= k < limit && k !in {i, j} ==> a[k] == old(a[k]);
{
|