From aec9290fbd3ca9ada5a7fad4dabb4ed1ffad6a84 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 28 Sep 2015 13:31:26 -0700
Subject: Additional tests

---
 Test/dafny0/CoPrefix.dfy                | 32 ++++++++++++++++++++++++++++++++
 Test/dafny0/CoPrefix.dfy.expect         | 17 ++++++++++++++++-
 Test/dafny0/ResolutionErrors.dfy        |  9 +++++++++
 Test/dafny0/ResolutionErrors.dfy.expect |  3 ++-
 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
-- 
cgit v1.2.3