From 5b3dcd0c09a7ea8a34e7f5e4b8800015b3b07e96 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@microsoft.com>
Date: Wed, 1 Jul 2015 12:37:54 -0700
Subject: Add the ability to specify how much "fuel" a function should have,
 i.e., how many times Z3 is permitted to unfold it's definition.  The new
 {:fuel} annotation can be added to the function itself, it which case it will
 apply to all uses of that function, or it can overridden within the scope of
 a module, function, method, iterator, calc, forall, while, assert, or assume.
  The general format is:

{:fuel functionName,lowFuel,highFuel}

When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.

The default fuel setting for recursive functions is 1,2.  Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care.  Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.
---
 Test/dafny0/Fuel.dfy.expect | 95 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 95 insertions(+)
 create mode 100644 Test/dafny0/Fuel.dfy.expect

(limited to 'Test/dafny0/Fuel.dfy.expect')

diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
new file mode 100644
index 00000000..4c180a9c
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -0,0 +1,95 @@
+Fuel.dfy(17,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(65,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Else
+Fuel.dfy(69,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Then
+    (0,0): anon7_Then
+Fuel.dfy(92,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(94,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(120,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(122,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(129,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(132,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(133,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(157,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Else
+    (0,0): anon9
+Fuel.dfy(200,56): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(245,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(247,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(280,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Then
+Fuel.dfy(335,27): Error: possible violation of function precondition
+Fuel.dfy(324,22): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,51): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,39): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(397,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(398,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(407,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 51 verified, 24 errors
-- 
cgit v1.2.3