diff options
| author |  Rustan Leino <unknown> | 2014-01-05 15:28:15 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-05 15:28:15 -0800 |
| commit | 9fcb57c00fd690da3a86dbc890bc32f6fc352079 (patch) | |
| tree | 6f7c8f83068cfb35ad230cded6b9c04b937086bf /Test/dafny0/Answer | |
| parent | 5049ea124fe4b34f5c8fcb244663f3b68053643e (diff) | |
Added ghost let expressions.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 5ef39185..0ce33b47 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -434,6 +434,10 @@ ResolutionErrors.dfy(735,19): Error: a while statement used inside a hint is not ResolutionErrors.dfy(760,4): Error: calls to methods with side-effects are not allowed inside a statement expression
ResolutionErrors.dfy(761,4): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(762,4): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(773,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(783,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(794,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(803,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(427,2): Error: More than one default constructor
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
@@ -507,7 +511,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(544,18): Error: unresolved identifier: w
ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses
-110 resolution/type errors detected in ResolutionErrors.dfy
+114 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -2320,7 +2324,7 @@ Dafny program verifier finished with 9 verified, 6 errors Dafny program verifier finished with 0 verified, 0 errors
-Dafny program verifier finished with 37 verified, 0 errors
+Dafny program verifier finished with 44 verified, 0 errors
Compiled assembly into Compilation.exe
Dafny program verifier finished with 9 verified, 0 errors
|