Improve Dafny's ability to find fueled functions by checking the function itself,

as well as the signature and body of other functions.

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1798243c..6ded74d5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -444,6 +444,13 @@ namespace Microsoft.Dafny
           } else if (clbl is IteratorDecl) {

             body = ((IteratorDecl)clbl).Body;

             CheckForFuelAdjustments(clbl.Tok, ((IteratorDecl)clbl).Attributes, module);

+          } else if (clbl is Function) {            

+            CheckForFuelAdjustments(clbl.Tok, ((Function)clbl).Attributes, module);

+            var c = new FuelAdjustment_Visitor(this);

+            var bodyExpr = ((Function)clbl).Body;

+            if (bodyExpr != null) {

+              c.Visit(bodyExpr, new FuelAdjustment_Context(module));

+            }

           }

           if (body != null) {

             var c = new FuelAdjustment_Visitor(this);