diff options
| author |  leino <unknown> | 2015-09-28 13:31:26 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:31:26 -0700 |
| commit | aec9290fbd3ca9ada5a7fad4dabb4ed1ffad6a84 (patch) | |
| tree | f1f8515675b958c319b94cee89d53422cf6053ff /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 4c21d765625b35eab9f5dc4ca21f170d3f7a2f04 (diff) | |
Additional tests
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index e5506688..6f4b3519 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -132,6 +132,7 @@ ResolutionErrors.dfy(1578,9): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(1584,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
ResolutionErrors.dfy(1601,8): Error: print 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(1610,26): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1618,6): Error: the type of the bound variable 't' could not be determined
ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -199,4 +200,4 @@ ResolutionErrors.dfy(1112,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1133,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1140,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1155,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-201 resolution/type errors detected in ResolutionErrors.dfy
+202 resolution/type errors detected in ResolutionErrors.dfy
|