diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 15:03:40 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-23 15:03:40 -0700 |
| commit | 4bcc3e82425441b077ff53a9c2b2a8442ff8936f (patch) | |
| tree | 503813442f8fb28a6a086ea15acb8ca8e1266e53 /Test/dafny0/UnfoldingPerformance.dfy.expect | |
| parent | 31005fdf54359aad3f33a54228d61d82e10bc679 (diff) | |
Fix: Read clauses should be checked before lit lifting
The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It
shouldn't be, because its reads clause is non-empty. This is not a soundness
bug, but fixing it improves performance in cases where a function call would be
incorrectly unrolled.
Test case written by Rustan.
Diffstat (limited to 'Test/dafny0/UnfoldingPerformance.dfy.expect')
| -rw-r--r-- | Test/dafny0/UnfoldingPerformance.dfy.expect | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/dafny0/UnfoldingPerformance.dfy.expect b/Test/dafny0/UnfoldingPerformance.dfy.expect new file mode 100644 index 00000000..220fecc5 --- /dev/null +++ b/Test/dafny0/UnfoldingPerformance.dfy.expect @@ -0,0 +1,11 @@ +UnfoldingPerformance.dfy(23,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+UnfoldingPerformance.dfy(30,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+UnfoldingPerformance.dfy(51,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 11 verified, 3 errors
|