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, 2 insertions, 4 deletions

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
index 52f5cf76..d5febfe0 100644
--- a/Test/dafny1/ListCopy.dfy
+++ b/Test/dafny1/ListCopy.dfy
@@ -19,8 +19,7 @@ class Node {
     var newRegion: set<Node> := {};

 

     if (oldListPtr != null) {

-      newRoot := new Node;

-      call newRoot.Init();

+      newRoot := new Node.Init();

       newRegion := newRegion + {newRoot};

       var prev := newRoot;

 

@@ -33,8 +32,7 @@ class Node {
         invariant newRegion !! existingRegion;

         decreases *;  // omit loop termination check

       {

-        var tmp := new Node;

-        call tmp.Init();

+        var tmp := new Node.Init();

 

         newRegion := newRegion + {tmp};

         prev.nxt := tmp;