Do postponsed reads checking also for the body of functions -- see Test/dafny0/Reads.dfy for benefits.

(Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect
index 62b67cc3..619a9c84 100644
--- a/Test/dafny0/Corecursion.dfy.expect
+++ b/Test/dafny0/Corecursion.dfy.expect
@@ -13,17 +13,17 @@ Execution trace:
 Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0