Disallow call-graph clusters that mix co-methods / prefix methods with other things.

Disallow call-graph clusters that mix co-predicates / prefix predicates with other things.

1 files changed, 13 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index f04c17a6..5b465788 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1978,6 +1978,19 @@ namespace Microsoft.Dafny
           }

         }

       }

+      protected override void VisitOneExpr(Expression expr)

+      {

+        if (expr is FunctionCallExpr) {

+          var e = (FunctionCallExpr)expr;

+          // the call goes from a comethod context to a non-comethod callee

+          var moduleCaller = context.EnclosingClass.Module;

+          var moduleCallee = e.Function.EnclosingClass.Module;

+          if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {

+            // we're looking at a recursive call (to a non-comethod)

+            Error(e.tok, "a recursive call from a comethod can go only to other comethods and prefix methods");

+          }

+        }

+      }

     }

     void CoMethodChecks(Statement stmt, CoMethod context) {

       Contract.Requires(stmt != null);