diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-19 15:35:32 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-19 15:35:32 -0800 |
| commit | 4e73a3397844fa7802854fd059a32b0c33c46de7 (patch) | |
| tree | 399eaedc8e1f1fc9d4e5ce4b6bacd0c85c22b808 /Test/dafny0/Answer | |
| parent | a0ab18fd4acd127715d273cf8ab163a4086fe359 (diff) | |
Dafny: for a datatype with just one constructor, don't check (but do assume) that destructors are applied only to those values constructed by that one-and-only constructor
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 8627da6a..aa58ac6e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1158,8 +1158,12 @@ Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype v Execution trace:
(0,0): anon0
(0,0): anon6_Then
+Datatypes.dfy(222,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T''
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Then
-Dafny program verifier finished with 29 verified, 5 errors
+Dafny program verifier finished with 32 verified, 6 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
|