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

6 files changed, 1 insertions, 22 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index a11dec52..4f717f48 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -94,7 +94,6 @@ class Benchmark3 {
    

     decreases |q.contents|;

     {  

-      var m,k;

       call m,k := RemoveMin(q);

       perm := perm + [p[k]]; //adds  index of min to perm

       p := p[k+1..]+ p[..k]; //remove index of min from p  

@@ -126,7 +125,6 @@ class Benchmark3 {
       invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far   

       decreases n-j;

     {

-		var x;

 		call x:= q.Dequeue();

 		call q.Enqueue(x);

 		if ( x < m) {k := j; m := x;}

@@ -140,7 +138,6 @@ class Benchmark3 {
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 

       decreases k-j;

     {     

-      var x;

       call x := q.Dequeue();

       call q.Enqueue(x);

       j:= j +1;

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ac58b7d1..5a9d46c8 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -30,7 +30,6 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       present := false;

@@ -55,7 +54,6 @@ class Map<Key,Value> {
     ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>

                 values[i] == old(values)[i]);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       keys := keys + [key];

@@ -88,7 +86,6 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&

               values[h..] == old(values)[h+1..]);

   {

-    var j;

     call j := FindIndex(key);

     if (0 <= j) {

       keys := keys[..j] + keys[j+1..];

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 9d384c38..8026e60f 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -99,7 +99,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);

@@ -113,7 +112,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/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index f6e7879f..48306e9b 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -114,7 +114,7 @@ class Client
 		call c.Add(45);

 		call c.Add(78);

 		

-		var iter,b,x, s:= [ ];

+		var s:= [ ];

 		

 		call iter:=c.GetIterator();

 		call b:= iter.MoveNext();

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 95267823..f7d51058 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -129,12 +129,10 @@ class Client {
 		call rd.Open();

 		

 		var q:= new Queue<int>;	

-		var ch;

 		while (true)

 		 invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

 		 decreases |rd.stream|;

 		{

-				var eos:bool;

 				call eos := rd.AtEndOfStream();

 				if (eos) 

 				{

@@ -146,7 +144,6 @@ class Client {
 	    }

 	    

 	    call rd.Close();

-	    var perm;

 	    call q,perm := Sort(q);

 	    

 	    var wr:= new Stream;

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 643609d0..51172419 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -61,7 +61,6 @@ class Glossary {
       //  ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)

       // we leave out the decreases clause - unbounded stream

     {

-      var term,definition;

       call term,definition := readDefinition(rs);

       if (term == null)

       {

@@ -72,7 +71,6 @@ class Glossary {
     }    

     

     call rs.Close();

-    var p;

     call q,p := Sort(q);

     var wr := new WriterStream;

     call wr.Create();

@@ -84,7 +82,6 @@ class Glossary {
       invariant q !in wr.footprint;

       decreases |q.contents|;

     {

-      var term, present, definition;

       call term:= q.Dequeue();

       call present,definition:= glossary.Find(term);

       assume present; // to change this into an assert we need the loop invariant ** above that we commented out

@@ -103,7 +100,6 @@ class Glossary {
         decreases |definition| -i;

       {

         var w := definition[i];

-        var d;

         assume w != null; // to convert this into an assert we need invariant *** above

         call present, d := glossary.Find(w);

         if (present)

@@ -135,7 +131,6 @@ class Glossary {
         invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

         invariant null !in definition;

       {

-        var w;

         call w := rs.GetWord();

         if (w == null)

         {

@@ -275,7 +270,6 @@ class Map<Key,Value> {
     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       present := false;

@@ -300,7 +294,6 @@ class Map<Key,Value> {
     ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>

                 values[i] == old(values)[i]);

   {

-    var j;

     call j := FindIndex(key);

     if (j == -1) {

       keys := keys + [key];

@@ -333,7 +326,6 @@ class Map<Key,Value> {
               keys[h..] == old(keys)[h+1..] &&

               values[h..] == old(values)[h+1..]);

   {

-    var j;

     call j := FindIndex(key);

     if (0 <= j) {

       keys := keys[..j] + keys[j+1..];