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);

4 files changed, 10 insertions, 18 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;

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);

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);

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);