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, 5 insertions, 8 deletions

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 94fe1eaa..d9bd36f5 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -31,8 +31,7 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - {this});

     ensures |contents| == 0;

   {

-    var n := new Node<T>;

-    call n.Init();

+    var n := new Node<T>.Init();

     head := n;

     tail := n;

     contents := n.tailContents;

@@ -53,8 +52,8 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents) + [t];

   {

-    var n := new Node<T>;

-    call n.Init();  n.data := t;

+    var n := new Node<T>.Init();

+    n.data := t;

     tail.next := n;

     tail := n;

 

@@ -150,10 +149,8 @@ class Node<T> {
 class Main<U> {

   method A<T>(t: T, u: T, v: T)

   {

-    var q0 := new Queue<T>;

-    call q0.Init();

-    var q1 := new Queue<T>;

-    call q1.Init();

+    var q0 := new Queue<T>.Init();

+    var q1 := new Queue<T>.Init();

 

     call q0.Enqueue(t);

     call q0.Enqueue(u);