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/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index bb88b265..3f30c4b5 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -54,8 +54,7 @@ class Benchmark3 {
     // the final Queue is a permutation of the input Queue

     ensures (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

   {

-    r := new Queue<int>;

-    call r.Init();

+    r := new Queue<int>.Init();

     ghost var p := [];

     

     var n := 0;