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/test2/Answer | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'Test/test2') diff --git a/Test/test2/Answer b/Test/test2/Answer index 5cea9721..ae27fa94 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -1,6 +1,6 @@ -------------------- FormulaTerm.bpl -------------------- -FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement. +FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold on this return path. FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold. Execution trace: FormulaTerm.bpl(8,1): start @@ -18,7 +18,7 @@ Execution trace: Boogie program verifier finished with 2 verified, 2 errors -------------------- Passification.bpl -------------------- -Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement. +Passification.bpl(44,3): Error BP5003: A postcondition might not hold on this return path. Passification.bpl(36,3): Related location: This is the postcondition that might not hold. Execution trace: Passification.bpl(39,1): A @@ -44,23 +44,23 @@ Boogie program verifier finished with 7 verified, 4 errors Boogie program verifier finished with 4 verified, 0 errors -------------------- Ensures.bpl -------------------- -Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(30,5): Error BP5003: A postcondition might not hold on this return path. Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: Ensures.bpl(28,3): start -Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(35,5): Error BP5003: A postcondition might not hold on this return path. Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: Ensures.bpl(34,3): start -Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(41,5): Error BP5003: A postcondition might not hold on this return path. Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: Ensures.bpl(39,3): start -Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(47,5): Error BP5003: A postcondition might not hold on this return path. Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: Ensures.bpl(45,3): start -Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(72,5): Error BP5003: A postcondition might not hold on this return path. Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. Execution trace: Ensures.bpl(70,3): start @@ -68,7 +68,7 @@ Execution trace: Boogie program verifier finished with 5 verified, 5 errors -------------------- Old.bpl -------------------- -Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement. +Old.bpl(29,5): Error BP5003: A postcondition might not hold on this return path. Old.bpl(26,3): Related location: This is the postcondition that might not hold. Execution trace: Old.bpl(28,3): start @@ -81,11 +81,11 @@ OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts 2 name resolution errors detected in OldIllegal.bpl -------------------- Arrays.bpl -------------------- -Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path. Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. Execution trace: Arrays.bpl(42,3): start -Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path. Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. Execution trace: Arrays.bpl(123,3): start @@ -128,7 +128,7 @@ Execution trace: Call.bpl(46,5): Error BP5001: This assertion might not hold. Execution trace: Call.bpl(45,3): start -Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement. +Call.bpl(55,5): Error BP5003: A postcondition might not hold on this return path. Call.bpl(20,3): Related location: This is the postcondition that might not hold. Execution trace: Call.bpl(53,3): start @@ -211,7 +211,7 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar 18 type checking errors detected in strings-where.bpl -------------------- Structured.bpl -------------------- -Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement. +Structured.bpl(252,14): Error BP5003: A postcondition might not hold on this return path. Structured.bpl(243,3): Related location: This is the postcondition that might not hold. Execution trace: Structured.bpl(244,5): anon0 @@ -382,11 +382,11 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors -------------------- Arrays.bpl /typeEncoding:m -------------------- -Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path. Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. Execution trace: Arrays.bpl(42,3): start -Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(127,5): Error BP5003: A postcondition might not hold on this return path. Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. Execution trace: Arrays.bpl(123,3): start @@ -442,7 +442,7 @@ Execution trace: Boogie program verifier finished with 10 verified, 8 errors -------------------- ContractEvaluationOrder.bpl -------------------- -ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement. +ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path. ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold. Execution trace: ContractEvaluationOrder.bpl(7,5): anon0 -- cgit v1.2.3