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

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 4c3b095a..940e1a0a 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();

     ensures content == [val] + old(content);

   {

-    var tmp := new Node<T>;

-    call tmp.InitNode(val,top);

+    var tmp := new Node<T>.InitNode(val,top);

     top := tmp;

     representation := representation + top.footprint;

     content := [val] + content;