From 88f5ac86bda56381f81be032a0011e34aeca50a8 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@microsoft.com>
Date: Mon, 19 Oct 2015 22:53:41 -0700
Subject: Improve Dafny's ability to find fueled functions by checking the
 function itself, as well as the signature and body of other functions.

---
 Source/Dafny/DafnyAst.cs | 20 ++++++++++++++++++++
 Source/Dafny/Resolver.cs |  7 +++++++
 2 files changed, 27 insertions(+)

(limited to 'Source')

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 667f8407..871d644d 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3202,7 +3202,27 @@ namespace Microsoft.Dafny {
       this.Decreases = decreases;
       this.Body = body;
       this.SignatureEllipsis = signatureEllipsis;
+
+      if (attributes != null) {
+        List<Expression> args = Attributes.FindExpressions(attributes, "fuel");
+        if (args != null) {
+          if (args.Count == 1) {
+            LiteralExpr literal = args[0] as LiteralExpr;
+            if (literal != null && literal.Value is BigInteger) {
+              this.IsFueled = true;
+            }
+          } else if (args.Count == 2) {
+            LiteralExpr literalLow = args[0] as LiteralExpr;
+            LiteralExpr literalHigh = args[1] as LiteralExpr;
+
+            if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) {
+              this.IsFueled = true;
+            }
+          }
+        }
+      }
     }
+          
 
     bool ICodeContext.IsGhost { get { return this.IsGhost; } }
     List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
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);
-- 
cgit v1.2.3