Dafny: Added definedness checks for all statements (previously, some were missing)

Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting

3 files changed, 49 insertions, 49 deletions

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
     var high := a.Length();

 

     while (low < high)

-      invariant 0 <= low && high <= a.Length();

+      invariant 0 <= low && low <= high && high <= a.Length();

       invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);

       invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));

       decreases high - low;

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index d45db684..37b73cba 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -61,10 +61,10 @@ class Benchmark3 {
     

     var n := 0;

 	while (n < |q.contents|)

-		invariant n <=|q.contents| ;

-		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		invariant n <= |q.contents|;

 		invariant n == |p|;

-		decreases |q.contents| -n;

+		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		decreases |q.contents| - n;

    {

 		p := p + [n];

 		n := n + 1;

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index d320f9e9..90f484bd 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -6,22 +6,22 @@ class Collection<T> {
   function Valid():bool

   reads this, footprint;

   {

-		this in footprint

+    this in footprint

   }

   

   method GetCount() returns (c:int)

   requires Valid();

   ensures 0<=c;

   {

-		c:=|elements|;

+    c:=|elements|;

   }

   

   method Init()

   modifies this;

   ensures Valid() && fresh(footprint -{this});

   {

-		elements := [];

-		footprint := {this}; 

+    elements := [];

+    footprint := {this}; 

   }

   

   method GetItem(i:int ) returns (x:T)

@@ -29,7 +29,7 @@ class Collection<T> {
   requires 0<=i && i<|elements|;

   ensures elements[i] ==x;

   {

-		x:=elements[i];

+    x:=elements[i];

   }

   

   method Add(x:T )

@@ -38,7 +38,7 @@ class Collection<T> {
   ensures Valid() && fresh(footprint - old(footprint));

   ensures elements == old(elements) + [x];

   {

-		elements:= elements + [x];

+    elements:= elements + [x];

   }

   

   method GetIterator() returns (iter:Iterator<T>)

@@ -63,7 +63,7 @@ class Iterator<T> {
   function Valid():bool

   reads this, footprint;

   {

-		this in footprint && c!= null && -1<= pos && null !in footprint

+    this in footprint && c!= null && -1<= pos && null !in footprint

   }

   

   method Init(coll:Collection<T>)

@@ -72,9 +72,9 @@ class Iterator<T> {
   ensures Valid() && fresh(footprint -{this}) && pos ==-1;

   ensures c == coll;

   {

-		c:= coll;

-		pos:=-1;

-		footprint := {this}; 

+    c:= coll;

+    pos:=-1;

+    footprint := {this}; 

   }

   

   method MoveNext() returns (b:bool)

@@ -83,22 +83,22 @@ class Iterator<T> {
   ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;

   ensures b == HasCurrent() && c == old(c);

   {

-	pos:= pos+1;

-	b:= pos < |c.elements|;

+  pos:= pos+1;

+  b:= pos < |c.elements|;

   }

   

  function HasCurrent():bool //???

- requires Valid();

- reads this, c;

+   requires Valid();

+   reads this, c;

  {

-	0<= pos && pos < |c.elements|

+  0<= pos && pos < |c.elements|

  }

  

  method GetCurrent() returns (x:T)

  requires Valid() && HasCurrent();

  ensures c.elements[pos] == x;

   {

-		x:=c.elements[pos];

+    x:=c.elements[pos];

   }

  

 } 

@@ -106,34 +106,34 @@ class Iterator<T> {
 class Client

 {

 

-	method Main()

-	{

-		var c:= new Collection<int>;

-		call c.Init();

-		call c.Add(33);

-		call c.Add(45);

-		call c.Add(78);

-		

-		var s:= [ ];

-		

-		call iter:=c.GetIterator();

-		call b:= iter.MoveNext();

-		

-		while (b)

-		invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();

-		invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints

-		invariant 0<= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;

-		invariant iter.c == c;

-		decreases |c.elements| - iter.pos;

-		{   

-			call x:= iter.GetCurrent();

-			s:= s + [x];

-			call b:= iter.MoveNext();

-		}

-		

-		assert s == c.elements; //verifies that the iterator returns the correct things

-		call c.Add(100);

-	}

-	

+  method Main()

+  {

+    var c:= new Collection<int>;

+    call c.Init();

+    call c.Add(33);

+    call c.Add(45);

+    call c.Add(78);

+    

+    var s:= [ ];

+    

+    call iter := c.GetIterator();

+    call b := iter.MoveNext();

+    

+    while (b)

+      invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);

+      invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints

+      invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;

+      invariant iter.c == c;

+      decreases |c.elements| - iter.pos;

+    {   

+      call x:= iter.GetCurrent();

+      s:= s + [x];

+      call b:= iter.MoveNext();

+    }

+    

+    assert s == c.elements; //verifies that the iterator returns the correct things

+    call c.Add(100);

+  }

+  

 }