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/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 9b244e69..13086f28 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -47,8 +47,7 @@ class Collection<T> {
     ensures fresh(iter.footprint) && iter.pos == -1;

     ensures iter.c == this;

   {

-      iter:= new Iterator<T>;

-      call iter.Init(this);

+      iter:= new Iterator<T>.Init(this);

   }

   

 }

@@ -107,8 +106,7 @@ class Client
 

   method Main()

   {

-    var c := new Collection<int>;

-    call c.Init();

+    var c := new Collection<int>.Init();

     call c.Add(33);

     call c.Add(45);

     call c.Add(78);