Dafny: retired the "call" keyword

1 files changed, 7 insertions, 7 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3359cff1..fcc764aa 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -109,11 +109,11 @@ class Modifies {
   method B(p: Modifies)

     modifies this;

   {

-    call A(this);

+    A(this);

     if (p == this) {

-      call p.A(p);

+      p.A(p);

     }

-    call A(p);  // error: may violate modifies clause

+    A(p);  // error: may violate modifies clause

   }

 

   method C(b: bool)

@@ -126,9 +126,9 @@ class Modifies {
     requires p != null;

   {

     if (y == 3) {

-      call p.C(true);  // error: may violate modifies clause

+      p.C(true);  // error: may violate modifies clause

     } else {

-      call p.C(false);  // error: may violation modifies clause (the check is done without regard

+      p.C(false);  // error: may violation modifies clause (the check is done without regard

                         // for the postcondition, which also makes sense, since there may, in

                         // principle, be other fields of the object that are not constrained by the

                         // postcondition)

@@ -138,7 +138,7 @@ class Modifies {
   method E()

     modifies this;

   {

-    call A(null);  // allowed

+    A(null);  // allowed

   }

 

   method F(s: set<Modifies>)

@@ -164,7 +164,7 @@ class Modifies {
       foreach (m in s) {

         m.x := m.x + 1;

       }

-      call F(s);

+      F(s);

     }

     foreach (m in s) {

       assert m.x < m.x + 10;  // nothing wrong with asserting something