diff options
| author |  Jason Koenig <unknown> | 2011-07-05 18:22:41 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-05 18:22:41 -0700 |
| commit | b5b29c378a82415e1d2b40528d06845f9c32d3ac (patch) | |
| tree | 4c363bfef9f1712188e4838ed7dace4091330463 /Test/dafny0/Answer | |
| parent | b3713a4e1f7feb345d93825d094a31450202e40f (diff) | |
Dafny: Updated regression tests to include chaining disjoint operators.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 384037ae..e5621773 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -450,12 +450,11 @@ ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(14,18): error: this operator cannot be part of a chain
ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-9 parse errors detected in ParseErrors.dfy
+8 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -1100,3 +1099,7 @@ ReturnErrors.dfy(41,10): Error: can only have initialization methods which modif -------------------- ReturnTests.dfy --------------------
Dafny program verifier finished with 16 verified, 0 errors
+
+-------------------- ChainingDisjointTests.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
|