Dafny: fixed regression tests

5 files changed, 27 insertions, 6 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c2ecdcf4..35a5017b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -510,7 +510,7 @@ ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowe
 ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

-ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

+ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

 ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

 ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name

 ResolutionErrors.dfy(55,7): Error: unresolved identifier: F

@@ -1557,6 +1557,16 @@ Execution trace:
 

 Dafny program verifier finished with 9 verified, 1 error

 

+-------------------- Maps.dfy --------------------

+Maps.dfy(76,8): Error: element may not be in domain

+Execution trace:

+    (0,0): anon0

+Maps.dfy(126,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 22 verified, 2 errors

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index 0bc1004f..e74873e3 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -80,7 +80,7 @@ method test8(a: array<int>, i: int, j: int)
 method test9(a: array<int>, i: int, j: int, limit: int)

    requires a != null && 0 <= i < j < limit <= a.Length;

    modifies a;

-   ensures old(multiset(a[0..limit])) == multiset(a[0..limit]);

+   ensures multiset(a[0..limit]) == old(multiset(a[0..limit]));

    ensures a[j] == old (a[i]) && a[i] == old(a[j]);

    ensures forall k :: 0 <= k < limit && k !in {i, j} ==> a[k] == old(a[k]);

 {

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 023d80df..9ed6d75a 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -115,6 +115,10 @@ Dafny program verifier finished with 15 verified, 4 errors
 

 Dafny program verifier finished with 10 verified, 0 errors

 

+-------------------- BDD.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

+

 -------------------- UltraFilter.dfy --------------------

 

 Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index 069ffbde..594be748 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -86,6 +86,13 @@ class Node<T> {
 

       reverse := current;

       current := nx;

+	  // This makes the verification go faster.

+	  assert current != null ==>

+        current.Valid() &&

+        current in old(footprint) && current.footprint <= old(footprint) &&

+        current.footprint !! reverse.footprint &&

+        |old(list)| == |reverse.list| + |current.list| &&

+        (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);

     }

   }

 }

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 8bed7545..835c3043 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -157,11 +157,11 @@ function last(xs: List): Nat
     case Cons(z, zs) => last(ys)

 }

 

-function map(f: FunctionValue, xs: List): List

+function apply(f: FunctionValue, xs: List): List

 {

   match xs

   case Nil => Nil

-  case Cons(y, ys) => Cons(Apply(f, y), map(f, ys))

+  case Cons(y, ys) => Cons(Apply(f, y), apply(f, ys))

 }

 

 // In the following two functions, parameter "p" stands for a predicate:  applying p and

@@ -355,7 +355,7 @@ ghost method P11()
 }

 

 ghost method P12()

-  ensures forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs));

+  ensures forall n, xs, f :: drop(n, apply(f, xs)) == apply(f, drop(n, xs));

 {

 }

 

@@ -506,7 +506,7 @@ ghost method P40()
 }

 

 ghost method P41()

-  ensures forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs));

+  ensures forall n, xs, f :: take(n, apply(f, xs)) == apply(f, take(n, xs));

 {

 }