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

---
 Source/Dafny/Resolver.cs | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d6393b02..762bcc7e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7382,6 +7382,19 @@ namespace Microsoft.Dafny
           }
           return candidates;
         }
+      } else if (expr is BinaryExpr) {
+        var e = (BinaryExpr)expr;
+        if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon) {
+          if (e.E0.Type.IsCoDatatype) {
+            // Co-datatype equality (and disequality) are as destructive as can be--in essence, they destruct the values indefinitely--so don't allow
+            // any co-recursive calls in the operands.
+            var r = CheckCoCalls(e.E0, false, null);
+            Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
+            r = CheckCoCalls(e.E1, false, null);
+            Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls, given that we pass in allowCallsWithinRecursiveCluster==false
+            return candidates;
+          }
+        }
       } else if (expr is MatchExpr) {
         var e = (MatchExpr)expr;
         var r = CheckCoCalls(e.Source, false, null);
@@ -7435,13 +7448,6 @@ namespace Microsoft.Dafny
           Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls
         }
         return CheckCoCalls(e.Body, allowCallsWithinRecursiveCluster, null);
-      } else if (expr is ComprehensionExpr) {
-        var e = (ComprehensionExpr)expr;
-        foreach (var ee in e.SubExpressions) {
-          var r = CheckCoCalls(ee, false, null);
-          Contract.Assert(r.Count == 0);  // follows from postcondition of CheckCoCalls
-        }
-        return candidates;
       }
 
       // Default handling:
-- 
cgit v1.2.3