From 141863d4677fc7bd7b2c6891d6f354b7d9237036 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 28 Jun 2013 11:25:52 -0700
Subject: Fixed unsoundness (and also allowed other, sound cases) in the
 admissability checks for co-recursive calls

---
 Test/dafny0/Answer          | 25 ++++++++++++++-----------
 Test/dafny0/Corecursion.dfy | 23 +++++++++++++++++++++++
 2 files changed, 37 insertions(+), 11 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 97097cfd..36a6eda9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1151,8 +1151,11 @@ Execution trace:
 Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause
 Execution trace:
     (0,0): anon3_Else
+Corecursion.dfy(63,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
+Execution trace:
+    (0,0): anon5_Else
 
-Dafny program verifier finished with 5 verified, 2 errors
+Dafny program verifier finished with 7 verified, 3 errors
 
 -------------------- CoResolution.dfy --------------------
 CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default
@@ -1696,36 +1699,36 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors
 
 -------------------- Superposition.dfy --------------------
-
+
 Verifying CheckWellformed$$_0_M0.C.M ...
   [0 proof obligations]  verified
-
+
 Verifying Impl$$_0_M0.C.M ...
   [4 proof obligations]  verified
-
+
 Verifying CheckWellformed$$_0_M0.C.P ...
   [4 proof obligations]  verified
-
+
 Verifying CheckWellformed$$_0_M0.C.Q ...
   [3 proof obligations]  error
 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon5_Else
-
+
 Verifying CheckWellformed$$_0_M0.C.R ...
   [3 proof obligations]  error
 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon5_Else
-
+
 Verifying CheckWellformed$$_1_M1.C.M ...
   [0 proof obligations]  verified
-
+
 Verifying Impl$$_1_M1.C.M ...
   [1 proof obligation]  verified
-
+
 Verifying CheckWellformed$$_1_M1.C.P ...
   [1 proof obligation]  error
 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
@@ -1734,10 +1737,10 @@ Execution trace:
     (0,0): anon7_Else
     (0,0): anon9_Then
     (0,0): anon6
-
+
 Verifying CheckWellformed$$_1_M1.C.Q ...
   [0 proof obligations]  verified
-
+
 Verifying CheckWellformed$$_1_M1.C.R ...
   [0 proof obligations]  verified
 
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index 0918d6f5..6d3a0e13 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -50,3 +50,26 @@ module CoRecursionNotUsed {
     Diverge(n)  // error: cannot prove termination
   }
 }
+
+// --------------------------------------------------
+
+module EqualityIsSuperDestructive {
+  codatatype Stream<T> = Cons(head: T, tail: Stream)
+
+  function F(s: Stream<int>): Stream<int>
+  {
+    // Co-recursive calls are not allowed in arguments of equality, so the following call to
+    // F(s) is a recursive call.
+    if Cons(1, F(s)) == Cons(1, Cons(1, s))  // error: cannot prove termination
+    then Cons(2, s) else Cons(1, s)
+  }
+
+  ghost method lemma(s: Stream<int>)
+  {
+    // The following three assertions follow from the definition of F, so F had better
+    // generate some error (which it does -- the recursive call to F in F does not terminate).
+    assert F(s) == Cons(1, s);
+    assert F(s) == Cons(2, s);
+    assert false;
+  }
+}
-- 
cgit v1.2.3