Dafny: Added support for an initializing call as part of the new-allocation syntax. What you previously would have written like:

  c := new C;
  call c.Init(x, y);

you can now write as:

  c := new C.Init(x, y);

1 files changed, 8 insertions, 0 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 6e8e2b72..cbab53bf 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -72,3 +72,11 @@ method DuplicateVarName(x: int) returns (y: int)
   var y := y;  // error: redeclaration of an out-parameter is not allowed (it is

                // treated like an outermost-scoped local in this regard)

 }

+

+// ---------------------

+

+method InitCalls() {

+  var c := new C.F(null, null);  // error: F is not a method

+  var d := new C.M(8);  // error: M has out parameters

+  var e := new C.Caller();

+}