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.

1 files changed, 21 insertions, 4 deletions

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)) {