1 files changed, 27 insertions, 0 deletions
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
+}