diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-02-16 13:55:58 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-02-16 13:55:58 -0800 |
| commit | b6f1378a4c1bcfa3d56408dd6d388333bbb365ae (patch) | |
| tree | 308fde4f26db9d5c3364ffee3c28eef138bcd52c /Test/dafny0/Answer | |
| parent | cb3aad4de1ca1b991bb64b4f65dd7fed8cd78eb2 (diff) | |
Dafny: allow various forms of leaving off type arguments in declarations
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 6f160a66..6c6b54eb 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -498,7 +498,9 @@ ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_ ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
-46 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<T$0>, expected GList<int>)
+48 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -1250,6 +1252,10 @@ Execution trace: Dafny program verifier finished with 12 verified, 3 errors
+-------------------- NoTypeArgs.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
-------------------- SplitExpr.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
|