From dce966347df8c56502145cf681a8df4d3a2d9e7b Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 29 Aug 2012 18:11:49 -0700 Subject: Dafny: fixed bug in checking postconditions of functions that mention the result the function itself --- Test/dafny0/Answer | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/Answer') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index f9b2c66e..ac5e6be5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -486,8 +486,12 @@ Execution trace: (0,0): anon0 (0,0): anon9_Then (0,0): anon3 +FunctionSpecifications.dfy(56,10): Error BP5003: A postcondition might not hold on this return path. +FunctionSpecifications.dfy(57,22): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon5_Else -Dafny program verifier finished with 3 verified, 3 errors +Dafny program verifier finished with 3 verified, 4 errors -------------------- ResolutionErrors.dfy -------------------- ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context -- cgit v1.2.3