From 4bcc3e82425441b077ff53a9c2b2a8442ff8936f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 23 Jul 2015 15:03:40 -0700 Subject: 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. --- Test/dafny0/UnfoldingPerformance.dfy.expect | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 Test/dafny0/UnfoldingPerformance.dfy.expect (limited to 'Test/dafny0/UnfoldingPerformance.dfy.expect') 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 -- cgit v1.2.3