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/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index a37f86e4..02c1a63a 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -47,10 +47,8 @@ class Glossary {
   {

     var rs:= new ReaderStream;

     call rs.Open();

-    var glossary := new Map<Word,seq<Word>>;

-    call glossary.Init();

-    var q:= new Queue<Word>;

-    call q.Init();

+    var glossary := new Map<Word,seq<Word>>.Init();

+    var q:= new Queue<Word>.Init();

     

     while (true)

       invariant rs.Valid() && fresh(rs.footprint);