diff options
author | 2015-07-01 12:37:54 -0700 | |
---|---|---|
committer | 2015-07-01 12:37:54 -0700 | |
commit | 5b3dcd0c09a7ea8a34e7f5e4b8800015b3b07e96 (patch) | |
tree | 98802ece97362936aadb83d73304f5d92de4a33b /Test/dafny0/Fuel.dfy.expect | |
parent | 43b94536ff657d92866634831e2adda2d90e0f8a (diff) |
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.
Diffstat (limited to 'Test/dafny0/Fuel.dfy.expect')
-rw-r--r-- | Test/dafny0/Fuel.dfy.expect | 95 |
1 files changed, 95 insertions, 0 deletions
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
|