diff options
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 3198df33..50c238fc 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -484,7 +484,8 @@ ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called w ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
-44 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+45 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -1154,8 +1155,15 @@ Execution trace: (0,0): anon0
(0,0): anon4_Else
(0,0): anon5_Then
+Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Execution trace:
+ (0,0): anon0
+Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Then
-Dafny program verifier finished with 29 verified, 3 errors
+Dafny program verifier finished with 29 verified, 5 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
|