Boogie:

* Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners.
* It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs.
Dafny:
* Ditto for its Parser.cs/Scanner.cs.
* Added ability to provide a custom Errors handler for scanner/parser.
* Added Test/dafny1/Cubes.dfy

1 files changed, 111 insertions, 111 deletions

diff --git a/Test/test2/Answer b/Test/test2/Answer
index ae27fa94..4c0cbfc1 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -3,17 +3,17 @@
 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

+    FormulaTerm.bpl(8,1): start

 

 Boogie program verifier finished with 11 verified, 1 error

 

 -------------------- FormulaTerm2.bpl --------------------

 FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        FormulaTerm2.bpl(36,3): start

+    FormulaTerm2.bpl(36,3): start

 FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        FormulaTerm2.bpl(45,3): start

+    FormulaTerm2.bpl(45,3): start

 

 Boogie program verifier finished with 2 verified, 2 errors

 

@@ -21,21 +21,21 @@ Boogie program verifier finished with 2 verified, 2 errors
 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

+    Passification.bpl(39,1): A

 Passification.bpl(116,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Passification.bpl(106,1): L0

-        Passification.bpl(111,1): L1

-        Passification.bpl(115,1): L2

+    Passification.bpl(106,1): L0

+    Passification.bpl(111,1): L1

+    Passification.bpl(115,1): L2

 Passification.bpl(151,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Passification.bpl(144,1): L0

-        Passification.bpl(150,1): L2

+    Passification.bpl(144,1): L0

+    Passification.bpl(150,1): L2

 Passification.bpl(165,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Passification.bpl(158,1): L0

-        Passification.bpl(161,1): L1

-        Passification.bpl(164,1): L2

+    Passification.bpl(158,1): L0

+    Passification.bpl(161,1): L1

+    Passification.bpl(164,1): L2

 

 Boogie program verifier finished with 7 verified, 4 errors

 

@@ -47,23 +47,23 @@ Boogie program verifier finished with 4 verified, 0 errors
 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(28,3): start

 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(34,3): start

 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(39,3): start

 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(45,3): start

 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

+    Ensures.bpl(70,3): start

 

 Boogie program verifier finished with 5 verified, 5 errors

 

@@ -71,7 +71,7 @@ Boogie program verifier finished with 5 verified, 5 errors
 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

+    Old.bpl(28,3): start

 

 Boogie program verifier finished with 7 verified, 1 error

 

@@ -84,75 +84,75 @@ OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts
 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(42,3): start

 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

+    Arrays.bpl(123,3): start

 

 Boogie program verifier finished with 8 verified, 2 errors

 

 -------------------- Axioms.bpl --------------------

 Axioms.bpl(19,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Axioms.bpl(18,3): start

+    Axioms.bpl(18,3): start

 

 Boogie program verifier finished with 2 verified, 1 error

 

 -------------------- Quantifiers.bpl --------------------

 Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(19,3): start

+    Quantifiers.bpl(19,3): start

 Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(42,3): start

+    Quantifiers.bpl(42,3): start

 Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(64,3): start

+    Quantifiers.bpl(64,3): start

 Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(71,3): start

+    Quantifiers.bpl(71,3): start

 Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(124,3): start

+    Quantifiers.bpl(124,3): start

 Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Quantifiers.bpl(149,3): start

+    Quantifiers.bpl(149,3): start

 

 Boogie program verifier finished with 8 verified, 6 errors

 

 -------------------- Call.bpl --------------------

 Call.bpl(13,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Call.bpl(9,3): entry

+    Call.bpl(9,3): entry

 Call.bpl(46,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        Call.bpl(45,3): start

+    Call.bpl(45,3): start

 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

+    Call.bpl(53,3): start

 

 Boogie program verifier finished with 2 verified, 3 errors

 

 -------------------- AssumeEnsures.bpl --------------------

 AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold.

 Execution trace:

-        AssumeEnsures.bpl(26,5): entry

+    AssumeEnsures.bpl(26,5): entry

 AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold.

 Execution trace:

-        AssumeEnsures.bpl(46,5): entry

+    AssumeEnsures.bpl(46,5): entry

 AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold.

 Execution trace:

-        AssumeEnsures.bpl(60,5): entry

+    AssumeEnsures.bpl(60,5): entry

 

 Boogie program verifier finished with 4 verified, 3 errors

 

 -------------------- CutBackEdge.bpl --------------------

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

 Execution trace:

-        CutBackEdge.bpl(5,3): entry

-        CutBackEdge.bpl(9,3): block850

+    CutBackEdge.bpl(5,3): entry

+    CutBackEdge.bpl(9,3): block850

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -163,8 +163,8 @@ Boogie program verifier finished with 2 verified, 0 errors
 -------------------- LoopInvAssume.bpl --------------------

 LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold.

 Execution trace:

-        LoopInvAssume.bpl(8,4): entry

-        LoopInvAssume.bpl(16,4): exit

+    LoopInvAssume.bpl(8,4): entry

+    LoopInvAssume.bpl(16,4): exit

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -214,170 +214,170 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar
 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

-        Structured.bpl(246,5): anon6_LoopBody

-        Structured.bpl(247,7): anon7_LoopBody

-        Structured.bpl(248,11): anon8_Then

-        Structured.bpl(252,5): anon4

-        Structured.bpl(252,14): anon9_Then

+    Structured.bpl(244,5): anon0

+    Structured.bpl(246,5): anon6_LoopBody

+    Structured.bpl(247,7): anon7_LoopBody

+    Structured.bpl(248,11): anon8_Then

+    Structured.bpl(252,5): anon4

+    Structured.bpl(252,14): anon9_Then

 Structured.bpl(303,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Structured.bpl(299,5): anon0

-        Structured.bpl(300,3): anon3_Else

-        Structured.bpl(303,3): anon2

+    Structured.bpl(299,5): anon0

+    Structured.bpl(300,3): anon3_Else

+    Structured.bpl(303,3): anon2

 Structured.bpl(311,7): Error BP5001: This assertion might not hold.

 Execution trace:

-        Structured.bpl(308,3): anon0

-        Structured.bpl(308,3): anon1_Then

-        Structured.bpl(309,5): A

+    Structured.bpl(308,3): anon0

+    Structured.bpl(308,3): anon1_Then

+    Structured.bpl(309,5): A

 

 Boogie program verifier finished with 15 verified, 3 errors

 

 -------------------- Where.bpl --------------------

 Where.bpl(8,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(6,3): anon0

+    Where.bpl(6,3): anon0

 Where.bpl(22,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(16,5): anon0

+    Where.bpl(16,5): anon0

 Where.bpl(32,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(30,3): anon0

+    Where.bpl(30,3): anon0

 Where.bpl(44,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(40,5): anon0

+    Where.bpl(40,5): anon0

 Where.bpl(57,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(52,3): anon0

+    Where.bpl(52,3): anon0

 Where.bpl(111,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(102,5): anon0

-        Where.bpl(104,3): anon3_LoopHead

-        Where.bpl(104,3): anon3_LoopDone

+    Where.bpl(102,5): anon0

+    Where.bpl(104,3): anon3_LoopHead

+    Where.bpl(104,3): anon3_LoopDone

 Where.bpl(128,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(121,5): anon0

-        Where.bpl(122,3): anon3_LoopHead

-        Where.bpl(122,3): anon3_LoopDone

+    Where.bpl(121,5): anon0

+    Where.bpl(122,3): anon3_LoopHead

+    Where.bpl(122,3): anon3_LoopDone

 Where.bpl(145,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(138,5): anon0

-        Where.bpl(139,3): anon3_LoopHead

-        Where.bpl(139,3): anon3_LoopDone

+    Where.bpl(138,5): anon0

+    Where.bpl(139,3): anon3_LoopHead

+    Where.bpl(139,3): anon3_LoopDone

 Where.bpl(162,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Where.bpl(155,5): anon0

-        Where.bpl(156,3): anon3_LoopHead

-        Where.bpl(156,3): anon3_LoopDone

+    Where.bpl(155,5): anon0

+    Where.bpl(156,3): anon3_LoopHead

+    Where.bpl(156,3): anon3_LoopDone

 

 Boogie program verifier finished with 2 verified, 9 errors

 

 -------------------- UpdateExpr.bpl --------------------

 UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        UpdateExpr.bpl(14,3): anon0

+    UpdateExpr.bpl(14,3): anon0

 UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        UpdateExpr.bpl(19,3): anon0

+    UpdateExpr.bpl(19,3): anon0

 UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        UpdateExpr.bpl(32,3): anon0

+    UpdateExpr.bpl(32,3): anon0

 UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        UpdateExpr.bpl(38,3): anon0

+    UpdateExpr.bpl(38,3): anon0

 UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        UpdateExpr.bpl(51,5): anon0

+    UpdateExpr.bpl(51,5): anon0

 

 Boogie program verifier finished with 5 verified, 5 errors

 

 -------------------- NeverPattern.bpl --------------------

 NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NeverPattern.bpl(15,3): anon0

+    NeverPattern.bpl(15,3): anon0

 NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NeverPattern.bpl(21,3): anon0

+    NeverPattern.bpl(21,3): anon0

 NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NeverPattern.bpl(27,3): anon0

+    NeverPattern.bpl(27,3): anon0

 

 Boogie program verifier finished with 1 verified, 3 errors

 

 -------------------- NullaryMaps.bpl --------------------

 NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NullaryMaps.bpl(28,3): anon0

+    NullaryMaps.bpl(28,3): anon0

 NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NullaryMaps.bpl(28,3): anon0

+    NullaryMaps.bpl(28,3): anon0

 NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NullaryMaps.bpl(36,3): anon0

+    NullaryMaps.bpl(36,3): anon0

 

 Boogie program verifier finished with 2 verified, 3 errors

 

 -------------------- Implies.bpl --------------------

 Implies.bpl(12,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(11,3): anon0

+    Implies.bpl(11,3): anon0

 Implies.bpl(15,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(11,3): anon0

+    Implies.bpl(11,3): anon0

 Implies.bpl(19,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(19,3): anon0

+    Implies.bpl(19,3): anon0

 Implies.bpl(24,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(24,3): anon0

+    Implies.bpl(24,3): anon0

 Implies.bpl(25,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(24,3): anon0

+    Implies.bpl(24,3): anon0

 Implies.bpl(29,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(29,3): anon0

+    Implies.bpl(29,3): anon0

 Implies.bpl(34,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(34,3): anon0

+    Implies.bpl(34,3): anon0

 Implies.bpl(35,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Implies.bpl(34,3): anon0

+    Implies.bpl(34,3): anon0

 

 Boogie program verifier finished with 0 verified, 8 errors

 

 -------------------- IfThenElse1.bpl --------------------

 IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        IfThenElse1.bpl(26,3): anon0

+    IfThenElse1.bpl(26,3): anon0

 IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        IfThenElse1.bpl(33,3): anon0

+    IfThenElse1.bpl(33,3): anon0

 

 Boogie program verifier finished with 2 verified, 2 errors

 

 -------------------- Lambda.bpl --------------------

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

 Execution trace:

-        Lambda.bpl(36,5): anon0

+    Lambda.bpl(36,5): anon0

 Lambda.bpl(38,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Lambda.bpl(36,5): anon0

+    Lambda.bpl(36,5): anon0

 

 Boogie program verifier finished with 4 verified, 2 errors

 

 -------------------- LambdaPoly.bpl --------------------

 LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        LambdaPoly.bpl(24,5): anon0

-        LambdaPoly.bpl(27,5): anon4_Then

+    LambdaPoly.bpl(24,5): anon0

+    LambdaPoly.bpl(27,5): anon4_Then

 LambdaPoly.bpl(31,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        LambdaPoly.bpl(24,5): anon0

-        LambdaPoly.bpl(30,5): anon5_Then

+    LambdaPoly.bpl(24,5): anon0

+    LambdaPoly.bpl(30,5): anon5_Then

 LambdaPoly.bpl(36,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        LambdaPoly.bpl(24,5): anon0

-        LambdaPoly.bpl(34,5): anon5_Else

+    LambdaPoly.bpl(24,5): anon0

+    LambdaPoly.bpl(34,5): anon5_Else

 

 Boogie program verifier finished with 1 verified, 3 errors

 

@@ -385,28 +385,28 @@ Boogie program verifier finished with 1 verified, 3 errors
 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(42,3): start

 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

+    Arrays.bpl(123,3): start

 

 Boogie program verifier finished with 8 verified, 2 errors

 

 -------------------- Lambda.bpl /typeEncoding:m --------------------

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

 Execution trace:

-        Lambda.bpl(36,5): anon0

+    Lambda.bpl(36,5): anon0

 Lambda.bpl(38,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        Lambda.bpl(36,5): anon0

+    Lambda.bpl(36,5): anon0

 

 Boogie program verifier finished with 4 verified, 2 errors

 

 -------------------- TypeEncodingM.bpl /typeEncoding:m --------------------

 TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        TypeEncodingM.bpl(11,9): anon0

+    TypeEncodingM.bpl(11,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 -------------------- sk_hack.bpl --------------------

@@ -416,28 +416,28 @@ Boogie program verifier finished with 1 verified, 0 errors
 -------------------- CallForall.bpl --------------------

 CallForall.bpl(17,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(17,3): anon0

+    CallForall.bpl(17,3): anon0

 CallForall.bpl(29,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(28,3): anon0

+    CallForall.bpl(28,3): anon0

 CallForall.bpl(41,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(40,3): anon0

+    CallForall.bpl(40,3): anon0

 CallForall.bpl(47,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(46,3): anon0

+    CallForall.bpl(46,3): anon0

 CallForall.bpl(75,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(75,3): anon0

+    CallForall.bpl(75,3): anon0

 CallForall.bpl(111,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(109,3): anon0

+    CallForall.bpl(109,3): anon0

 CallForall.bpl(118,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(117,3): anon0

+    CallForall.bpl(117,3): anon0

 CallForall.bpl(125,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        CallForall.bpl(124,3): anon0

+    CallForall.bpl(124,3): anon0

 

 Boogie program verifier finished with 10 verified, 8 errors

 

@@ -445,13 +445,13 @@ Boogie program verifier finished with 10 verified, 8 errors
 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

+    ContractEvaluationOrder.bpl(7,5): anon0

 ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        ContractEvaluationOrder.bpl(12,5): anon0

+    ContractEvaluationOrder.bpl(12,5): anon0

 ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.

 ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.

 Execution trace:

-        ContractEvaluationOrder.bpl(23,5): anon0

+    ContractEvaluationOrder.bpl(23,5): anon0

 

 Boogie program verifier finished with 1 verified, 3 errors