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, 3 insertions, 4 deletions

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 810931be..b790eea5 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -90,8 +90,8 @@ class ExtensibleArray<T> {
       elements[length - M] := t;

     } else {

       if (more == null) {

-        var mr := new ExtensibleArray<array<T>>;  more := mr;

-        call mr.Init();

+        var mr := new ExtensibleArray<array<T>>.Init();

+        more := mr;

         Repr := Repr + {mr} + mr.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

@@ -108,8 +108,7 @@ class ExtensibleArray<T> {
 }

 

 method Main() {

-  var a := new ExtensibleArray<int>;

-  call a.Init();

+  var a := new ExtensibleArray<int>.Init();

   var n := 0;

   while (n < 256*256+600)

     invariant a.Valid() && fresh(a.Repr);