diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 27 |
2 files changed, 31 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
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index cacc34be..9e7ad3b2 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -253,3 +253,30 @@ method DuplicateLabels(n: int) { x := x + 1;
label DuplicateLabel: x := x + 1;
}
+
+// --------------- constructors -------------------------------------
+
+class ClassWithConstructor {
+ var y: int;
+ method NotTheOne() { }
+ constructor InitA() { }
+ constructor InitB() modifies this; { y := 20; }
+}
+
+class ClassWithoutConstructor {
+ method Init() modifies this; { }
+}
+
+method ConstructorTests()
+{
+ var o := new object; // fine: does not have any constructors
+
+ o := new ClassWithoutConstructor; // fine: don't need to call anything particular method
+ o := new ClassWithoutConstructor.Init(); // this is also fine
+
+ var c := new ClassWithConstructor.InitA();
+ c := new ClassWithConstructor; // error: must call a constructor
+ c := new ClassWithConstructor.NotTheOne(); // error: must call a constructor, not an arbitrary method
+ c := new ClassWithConstructor.InitB();
+ c.InitB(); // error: not allowed to call constructors except during allocation
+}
|