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

5 files changed, 82 insertions, 82 deletions

diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer
index 55709034..9c22ca61 100644
--- a/Test/codeexpr/Answer
+++ b/Test/codeexpr/Answer
@@ -13,7 +13,7 @@ Execution trace:
 Boogie program verifier finished with 3 verified, 3 errors

 

 ------------------------------ CodeExpr1.bpl ---------------------

-CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.

+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold on this return path.

 CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.

 Execution trace:

         CodeExpr1.bpl(42,3): start

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 12cb5960..0820093a 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1,8 +1,8 @@
 -------------------- test0.bpl --------------------

 test0.bpl(30,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    test0.bpl(26,3): anon0

-    test0.bpl(30,5): anon3_Then

+        test0.bpl(26,3): anon0

+        test0.bpl(30,5): anon3_Then

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- test1.bpl --------------------

@@ -819,44 +819,44 @@ implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bo
 }

 

 

-<console>(68,4): Error BP5003: A postcondition might not hold at this return statement.

+<console>(68,4): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

-    <console>(19,0): anon0

-    <console>(28,0): inline$find$0$anon0

-    <console>(38,0): inline$find$0$anon4_LoopBody

-    <console>(42,0): inline$check$0$Entry

-    <console>(57,0): inline$check$0$anon4_Else

-    <console>(62,0): inline$check$0$anon3

-    <console>(65,0): inline$check$0$Return

+        <console>(19,0): anon0

+        <console>(28,0): inline$find$0$anon0

+        <console>(38,0): inline$find$0$anon4_LoopBody

+        <console>(42,0): inline$check$0$Entry

+        <console>(57,0): inline$check$0$anon4_Else

+        <console>(62,0): inline$check$0$anon3

+        <console>(65,0): inline$check$0$Return

 <console>(100,4): Error BP5001: This assertion might not hold.

 Execution trace:

-    <console>(19,0): anon0

-    <console>(28,0): inline$find$0$anon0

-    <console>(38,0): inline$find$0$anon4_LoopBody

-    <console>(42,0): inline$check$0$Entry

-    <console>(52,0): inline$check$0$anon4_Then

-    <console>(65,0): inline$check$0$Return

-    <console>(73,0): inline$find$0$anon5_Then

-    <console>(87,0): inline$find$0$anon3

-    <console>(90,0): inline$find$0$Return

-    <console>(95,0): anon0$1

-    <console>(98,0): anon3_Then

-<console>(50,4): Error BP5003: A postcondition might not hold at this return statement.

+        <console>(19,0): anon0

+        <console>(28,0): inline$find$0$anon0

+        <console>(38,0): inline$find$0$anon4_LoopBody

+        <console>(42,0): inline$check$0$Entry

+        <console>(52,0): inline$check$0$anon4_Then

+        <console>(65,0): inline$check$0$Return

+        <console>(73,0): inline$find$0$anon5_Then

+        <console>(87,0): inline$find$0$anon3

+        <console>(90,0): inline$find$0$Return

+        <console>(95,0): anon0$1

+        <console>(98,0): anon3_Then

+<console>(50,4): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

-    <console>(10,0): anon0

-    <console>(20,0): anon4_LoopBody

-    <console>(24,0): inline$check$0$Entry

-    <console>(39,0): inline$check$0$anon4_Else

-    <console>(44,0): inline$check$0$anon3

-    <console>(47,0): inline$check$0$Return

-<console>(99,0): Error BP5003: A postcondition might not hold at this return statement.

+        <console>(10,0): anon0

+        <console>(20,0): anon4_LoopBody

+        <console>(24,0): inline$check$0$Entry

+        <console>(39,0): inline$check$0$anon4_Else

+        <console>(44,0): inline$check$0$anon3

+        <console>(47,0): inline$check$0$Return

+<console>(99,0): Error BP5003: A postcondition might not hold on this return path.

 <console>(78,2): Related location: This is the postcondition that might not hold.

 Execution trace:

-    <console>(85,0): anon0

-    <console>(93,0): anon4_Else

-    <console>(98,0): anon3

+        <console>(85,0): anon0

+        <console>(93,0): anon4_Else

+        <console>(98,0): anon3

 

 Boogie program verifier finished with 0 verified, 4 errors

 -------------------- test6.bpl --------------------

@@ -1442,10 +1442,10 @@ Boogie program verifier finished with 5 verified, 0 errors
 -------------------- test5.bpl --------------------

 test5.bpl(37,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    test5.bpl(34,10): anon0

-    test5.bpl(28,10): inline$P$0$anon0

-    test5.bpl(28,10): inline$P$1$anon0

-    test5.bpl(34,10): anon0$2

+        test5.bpl(34,10): anon0

+        test5.bpl(28,10): inline$P$0$anon0

+        test5.bpl(28,10): inline$P$1$anon0

+        test5.bpl(34,10): anon0$2

 

 Boogie program verifier finished with 4 verified, 1 error

 -------------------- expansion.bpl --------------------

@@ -1465,37 +1465,37 @@ expansion.bpl(33,22): Error: expansion: an identifier was used more than once
 *** more than one possible expansion for x1

 expansion3.bpl(18,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    expansion3.bpl(18,3): anon0

+        expansion3.bpl(18,3): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- Elevator.bpl --------------------

 Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

-    Elevator.bpl(15,3): anon0

-    Elevator.bpl(15,3): anon0$1

-    Elevator.bpl(16,3): anon10_LoopHead

-    Elevator.bpl(19,5): anon10_LoopBody

-    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(24,7): anon13_Then$1

+        Elevator.bpl(15,3): anon0

+        Elevator.bpl(15,3): anon0$1

+        Elevator.bpl(16,3): anon10_LoopHead

+        Elevator.bpl(19,5): anon10_LoopBody

+        Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

+        Elevator.bpl(24,7): anon13_Then$1

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- Elevator.bpl with empty blocks --------------------

 Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

-    Elevator.bpl(15,3): anon0

-    Elevator.bpl(68,23): inline$Initialize$0$Entry

-    Elevator.bpl(71,13): inline$Initialize$0$anon0

-    Elevator.bpl(68,23): inline$Initialize$0$Return

-    Elevator.bpl(15,3): anon0$1

-    Elevator.bpl(16,3): anon10_LoopHead

-    Elevator.bpl(19,5): anon10_LoopBody

-    Elevator.bpl(19,5): anon11_Else

-    Elevator.bpl(19,5): anon12_Else

-    Elevator.bpl(24,7): anon13_Then

-    Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry

-    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

-    Elevator.bpl(94,23): inline$MoveDown_Error$0$Return

-    Elevator.bpl(24,7): anon13_Then$1

+        Elevator.bpl(15,3): anon0

+        Elevator.bpl(68,23): inline$Initialize$0$Entry

+        Elevator.bpl(71,13): inline$Initialize$0$anon0

+        Elevator.bpl(68,23): inline$Initialize$0$Return

+        Elevator.bpl(15,3): anon0$1

+        Elevator.bpl(16,3): anon10_LoopHead

+        Elevator.bpl(19,5): anon10_LoopBody

+        Elevator.bpl(19,5): anon11_Else

+        Elevator.bpl(19,5): anon12_Else

+        Elevator.bpl(24,7): anon13_Then

+        Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry

+        Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

+        Elevator.bpl(94,23): inline$MoveDown_Error$0$Return

+        Elevator.bpl(24,7): anon13_Then$1

 

 Boogie program verifier finished with 1 verified, 1 error

 -------------------- expansion2.bpl --------------------

@@ -1528,7 +1528,7 @@ axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
 Boogie program verifier finished with 0 verified, 0 errors

 fundef2.bpl(6,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    fundef2.bpl(5,3): anon0

+        fundef2.bpl(5,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 -------------------- polyInline.bpl --------------------

@@ -1537,10 +1537,10 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating
 polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int

 polyInline.bpl(23,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(20,3): anon0

+        polyInline.bpl(20,3): anon0

 polyInline.bpl(39,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(27,3): anon0

+        polyInline.bpl(27,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

 polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int

@@ -1548,9 +1548,9 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating
 polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int

 polyInline.bpl(23,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(20,3): anon0

+        polyInline.bpl(20,3): anon0

 polyInline.bpl(39,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    polyInline.bpl(27,3): anon0

+        polyInline.bpl(27,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer
index ecb258a2..1feac694 100644
--- a/Test/lazyinline/Answer
+++ b/Test/lazyinline/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

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

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