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 /Test/dafny0/Fuel.dfy | |
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 'Test/dafny0/Fuel.dfy')
-rw-r--r-- | Test/dafny0/Fuel.dfy | 39 |
1 files changed, 39 insertions, 0 deletions
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
+ }
+}
+
|