diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 20 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 | ||||
| -rw-r--r-- | Test/dafny0/Fuel.dfy | 39 | ||||
| -rw-r--r-- | Test/dafny0/Fuel.dfy.expect | 14 |
4 files changed, 79 insertions, 1 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);
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy index c8a1fc2f..abbc831e 100644 --- a/Test/dafny0/Fuel.dfy +++ b/Test/dafny0/Fuel.dfy @@ -421,3 +421,42 @@ module TestModule9 { }
}
+// Test fuel when it's applied to a non-recursive function directly (to simulate opaque)
+module TestModule10 {
+ function {:fuel 0,0} abs(x:int) : int
+ {
+ if x < 0 then -1 * x else x
+ }
+
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs(z) == -1*z; // error: Cannot see the body of abs
+ assert abs(y) == y; // error: Cannot see the body of abs
+ assert abs(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+}
+
+// Test fuel when it's mentioned in other functions function to simulate a local opaque
+module TestModule11 {
+ function abs(x:int) : int
+ {
+ if x < 0 then -1 * x else x
+ }
+
+ function {:fuel abs,0,0} abs'(x:int) : int
+ {
+ abs(x)
+ }
+
+ method test1(y:int, z:int)
+ requires y > 5;
+ requires z < 0;
+ {
+ assert abs'(z) == -1*z; // error: Cannot see the body of abs
+ assert abs'(y) == y; // error: Cannot see the body of abs
+ assert abs'(-1) == 1; // lit bypasses fuel, so this should succeed
+ }
+}
+
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index 90fe877d..0c128941 100644 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -91,5 +91,17 @@ Execution trace: Fuel.dfy(407,38): Error: assertion violation
Execution trace:
(0,0): anon0
+Fuel.dfy(435,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(436,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(457,23): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Fuel.dfy(458,23): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 51 verified, 24 errors
+Dafny program verifier finished with 56 verified, 28 errors
|