diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-28 18:08:55 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:08:55 -0700 |
| commit | c86a3199caf050ef4af4ce5873ee7d6a27b501ab (patch) | |
| tree | 47c42020587bffe014d52542bf8434b4a3a26683 /Test/dafny0/Answer | |
| parent | c7c9cd675bf6024a8f725c84fe22e17d3deb7a98 (diff) | |
Dafny: added constructors
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 05250fa8..0eab5c50 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -432,7 +432,10 @@ ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(252,2): Error: duplicate label
-38 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(278,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(279,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(281,4): Error: a constructor is only allowed to be called when an object is being allocated
+41 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
|