diff options
| author |  Bryan Parno <parno@microsoft.com> | 2015-10-19 22:53:41 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2015-10-19 22:53:41 -0700 |
| commit | 88f5ac86bda56381f81be032a0011e34aeca50a8 (patch) | |
| tree | 08cfa5f7b5d3896f9a8538291a9d584316b29daa /Source | |
| parent | be08f2949d674bd757a804795de1dd37c95177f3 (diff) | |
Improve Dafny's ability to find fueled functions by checking the function itself,
as well as the signature and body of other functions.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 20 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 |
2 files changed, 27 insertions, 0 deletions
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);
|