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.

---
 Test/dafny0/Fuel.dfy        | 39 +++++++++++++++++++++++++++++++++++++++
 Test/dafny0/Fuel.dfy.expect | 14 +++++++++++++-
 2 files changed, 52 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0')

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
@@ -89,7 +89,19 @@ Fuel.dfy(398,22): Error: assertion violation
 Execution trace:
     (0,0): anon0
 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
-- 
cgit v1.2.3