The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.

4 files changed, 0 insertions, 15 deletions

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 7a5fb3c7..138a22df 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -42,7 +42,6 @@ class IntSet {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents) + {x};

   { 

-    var t;

     call t := InsertHelper(x, root);

     root := t;

     contents := root.contents;

@@ -64,12 +63,10 @@ class IntSet {
       m := n;

     } else {

       if (x < n.data) {

-        var t;

         call t := InsertHelper(x, n.left);

         n.left := t;

         n.footprint := n.footprint + n.left.footprint;

       } else {

-        var t;

         call t := InsertHelper(x, n.right);

         n.right := t;

         n.footprint := n.footprint + n.right.footprint;

@@ -86,7 +83,6 @@ class IntSet {
     ensures contents == old(contents) - {x};

   {

     if (root != null) {

-      var newRoot;

       call newRoot := root.Remove(x);

       root := newRoot;

       if (root == null) {

@@ -169,13 +165,11 @@ class Node {
   {

     node := this;

     if (left != null && x < data) {

-      var t;

       call t := left.Remove(x);

       left := t;

       contents := contents - {x};

       if (left != null) { footprint := footprint + left.footprint; }

     } else if (right != null && data < x) {

-      var t;

       call t := right.Remove(x);

       right := t;

       contents := contents - {x};

@@ -189,7 +183,6 @@ class Node {
         node := left;

       } else {

         // rotate

-        var min, r;

         call min, r := right.RemoveMin();

         data := min;  right := r;

         contents := contents - {x};

@@ -211,7 +204,6 @@ class Node {
       min := data;

       node := right;

     } else {

-      var t;

       call min, t := left.RemoveMin();

       left := t;

       node := this;

@@ -229,7 +221,6 @@ class Main {
 

     call s.Insert(12);

     call s.Insert(24);

-    var present;

     call present := s.Find(x);

     assert present <==> x == 12 || x == 24;

   }

diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy
index ab83a75d..5c22ec92 100644
--- a/Test/dafny0/Queue.dfy
+++ b/Test/dafny0/Queue.dfy
@@ -49,7 +49,6 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents)[1..] + old(contents)[..1];

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -63,7 +62,6 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

-    var t: T;

     call t := Front();

     call Dequeue();

     call Enqueue(t);

@@ -163,7 +161,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

@@ -191,7 +188,6 @@ class Main<U> {
 

     assert |q0.contents| == 2;

 

-    var w;

     call w := q0.Front();

     assert w == t;

     call q0.Dequeue();

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 43fe63df..ee9d9613 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -28,7 +28,6 @@ class Termination {
   }

 

   method Lex() {

-    var x: int, y: int;

     call x := Update();

     call y := Update();

     while (!(x == 0 && y == 0))

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a5764be5..3f57f369 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -13,7 +13,6 @@ class C<U> {
   method Main(u: U)

   {

     var t := F(3,u) && F(this,u);

-    var kz;

     call kz := M(t,u);

     assert kz && (G() || !G());

   }