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

1 files changed, 15 insertions, 15 deletions

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