From b32f277e00ed5c3f90d01c17bcce0d8855eadfff Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 14 Sep 2010 20:09:39 +0000 Subject: Dafny: * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations --- Test/stratifiedinline/Answer | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/stratifiedinline') diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aa83b37c..290059d6 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl -bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement. +bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path. bar1.bpl(21,1): Related location: This is the postcondition that might not hold. Execution trace: bar1.bpl(24,3): anon0 @@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar3.bpl -bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement. +bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path. bar3.bpl(34,1): Related location: This is the postcondition that might not hold. Execution trace: bar3.bpl(38,3): anon0 -- cgit v1.2.3