Additional tests

4 files changed, 59 insertions, 2 deletions

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 0becb24d..3b6bd670 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -192,3 +192,35 @@ module Recursion {
     }

   }

 }

+

+module PrefixEquality {

+  codatatype Stream<T> = Cons(head: T, Stream)

+    

+  colemma Test0(s: Stream, t: Stream)

+    requires s.head == t.head

+  {

+    calc {

+      s;

+      ==#[_k-1]

+      t;  // error: this step might not hold

+      ==#[if 2 <= _k then _k-2 else _k-1]

+      s;  // error: this step might not hold

+      ==#[0]

+      t;

+    }

+  }

+

+  colemma Test1(s: Stream, t: Stream)

+    requires s == t

+  {

+    calc {

+      s;

+      ==#[_k-1]

+      t;

+      ==#[_k-2]  // error: prefix-equality limit must be at least 0

+      s;

+      ==#[0]

+      t;

+    }

+  }

+}

diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect
index a7295367..b42f2593 100644
--- a/Test/dafny0/CoPrefix.dfy.expect
+++ b/Test/dafny0/CoPrefix.dfy.expect
@@ -12,6 +12,21 @@ CoPrefix.dfy(176,10): Error: cannot prove termination; try supplying a decreases
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

+CoPrefix.dfy(205,6): Error: the calculation step between the previous line and this line might not hold

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon10_Then

+CoPrefix.dfy(207,6): Error: the calculation step between the previous line and this line might not hold

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon11_Then

+CoPrefix.dfy(220,12): Error: prefix-equality limit must be at least 0

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon11_Then

 CoPrefix.dfy(63,56): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

@@ -47,4 +62,4 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Else

 

-Dafny program verifier finished with 41 verified, 9 errors

+Dafny program verifier finished with 43 verified, 12 errors

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index a4161a46..9d4d67f1 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1610,3 +1610,12 @@ module MoreLetSuchThatExpr {
     var x := var y :| y < z; y;  // error: contraint depend on ghost (z)

   }

 }

+

+module UnderspecifiedTypedShouldBeResolvedOnlyOnce {

+  method CalcTest0(s: seq<int>) {

+    calc {

+      2;

+      var t :| true; 2;  // error: type of 't' is underspecified

+    }

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index e5506688..6f4b3519 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -132,6 +132,7 @@ ResolutionErrors.dfy(1578,9): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(1584,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost

 ResolutionErrors.dfy(1601,8): Error: print 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(1610,26): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(1618,6): Error: the type of the bound variable 't' could not be determined

 ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

@@ -199,4 +200,4 @@ ResolutionErrors.dfy(1112,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1133,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1140,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1155,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-201 resolution/type errors detected in ResolutionErrors.dfy

+202 resolution/type errors detected in ResolutionErrors.dfy