From e5fcbeda373f505f4ebfd29cafe776d9ec7b8db5 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 8 May 2010 02:19:17 +0000
Subject: Dafny: Previously, a "use" function was one whose definition was
 applied only in limited ways, namely when the function was uttered in a
 program (possibly in a "use" statement).  Now, recursive functions are always
 limited, unless declared with the new modifier "unlimited".  Non-recursive
 functions are always unlimited.  Also new is that only function calls within
 the same SCC of the call graph use the limited form of the callee. The "use"
 modifier is no longer supported.  The "use" statement is still supported, now
 for both limited and unlimited functions; but it's probably better and easier
 to just explicitly mention a function in an assertion, if needed.

---
 Source/Dafny/Resolver.ssc | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

(limited to 'Source/Dafny/Resolver.ssc')

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index db6e667a..e0efaa3c 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -92,6 +92,24 @@ namespace Microsoft.Dafny {
       foreach (ModuleDecl m in prog.Modules) {
         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
       }
+      // compute IsRecursive bit for mutually recursive functions
+      foreach (ModuleDecl m in prog.Modules) {
+        foreach (TopLevelDecl decl in m.TopLevelDecls) {
+          ClassDecl cl = decl as ClassDecl;
+          if (cl != null) {
+            foreach (MemberDecl member in cl.Members) {
+              Function fn = member as Function;
+              if (fn != null && !fn.IsRecursive) {  // note, self-recursion has already been determined
+                int n = m.CallGraph.GetSCCSize(fn);
+                if (2 <= n) {
+                  // the function is mutually recursive (note, the SCC does not determine self recursion)
+                  fn.IsRecursive = true;
+                }
+              }
+            }
+          }
+        }
+      }
     }
     
     public void RegisterTopLevelDecls(List<TopLevelDecl!>! declarations) {
@@ -808,10 +826,6 @@ namespace Microsoft.Dafny {
             break;
           }
         }
-        FunctionCallExpr fce = expr as FunctionCallExpr;
-        if (fce == null || fce.Function == null || !fce.Function.IsUse) {
-          Error(s.Expr, "use statement must indicate a function declared as use");
-        }
       } else if (stmt is PredicateStmt) {
         PredicateStmt s = (PredicateStmt)stmt;
         s.IsGhost = true;
@@ -1590,6 +1604,9 @@ namespace Microsoft.Dafny {
             if (callerModule == calleeModule) {
               // intra-module call; this is allowed; add edge in module's call graph
               callerModule.CallGraph.AddEdge(currentFunction, function);
+              if (currentFunction == function) {
+                currentFunction.IsRecursive = true;  // self recursion (mutual recursion is determined elsewhere)
+              }
             } else if (calleeModule.IsDefaultModule) {
               // all is fine: everything implicitly imports the default module
             } else if (importGraph.Reaches(callerModule, calleeModule)) {
-- 
cgit v1.2.3