From 356ebe6de99459cfb89920b18124aae016206ef0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 16:24:51 +0100 Subject: Enabled VC Generation lit tests. --- Test/test2/Answer | 622 +++++++++++++------------- Test/test2/Arrays.bpl | 4 + Test/test2/Arrays.bpl.expect | 10 + Test/test2/AssumeEnsures.bpl | 2 + Test/test2/AssumeEnsures.bpl.expect | 11 + Test/test2/AssumptionVariables0.bpl | 2 + Test/test2/AssumptionVariables0.bpl.expect | 11 + Test/test2/Axioms.bpl | 2 + Test/test2/Axioms.bpl.expect | 5 + Test/test2/B.bpl | 2 + Test/test2/B.bpl.expect | 2 + Test/test2/Call.bpl | 2 + Test/test2/Call.bpl.expect | 12 + Test/test2/ContractEvaluationOrder.bpl | 2 + Test/test2/ContractEvaluationOrder.bpl.expect | 13 + Test/test2/CutBackEdge.bpl | 2 + Test/test2/CutBackEdge.bpl.expect | 13 + Test/test2/Ensures.bpl | 2 + Test/test2/Ensures.bpl.expect | 22 + Test/test2/False.bpl | 2 + Test/test2/False.bpl.expect | 2 + Test/test2/FormulaTerm.bpl | 2 + Test/test2/FormulaTerm.bpl.expect | 6 + Test/test2/FormulaTerm2.bpl | 2 + Test/test2/FormulaTerm2.bpl.expect | 8 + Test/test2/FreeCall.bpl | 2 + Test/test2/FreeCall.bpl.expect | 18 + Test/test2/IfThenElse1.bpl | 2 + Test/test2/IfThenElse1.bpl.expect | 8 + Test/test2/Implies.bpl | 2 + Test/test2/Implies.bpl.expect | 26 ++ Test/test2/Lambda.bpl | 4 + Test/test2/Lambda.bpl.expect | 8 + Test/test2/LambdaOldExpressions.bpl | 2 + Test/test2/LambdaOldExpressions.bpl.expect | 6 + Test/test2/LambdaPoly.bpl | 2 + Test/test2/LambdaPoly.bpl.expect | 14 + Test/test2/LoopInvAssume.bpl | 2 + Test/test2/LoopInvAssume.bpl.expect | 6 + Test/test2/NeverPattern.bpl | 2 + Test/test2/NeverPattern.bpl.expect | 11 + Test/test2/NullaryMaps.bpl | 2 + Test/test2/NullaryMaps.bpl.expect | 11 + Test/test2/Old.bpl | 2 + Test/test2/Old.bpl.expect | 6 + Test/test2/OldIllegal.bpl | 2 + Test/test2/OldIllegal.bpl.expect | 3 + Test/test2/Passification.bpl | 2 + Test/test2/Passification.bpl.expect | 20 + Test/test2/Quantifiers.bpl | 2 + Test/test2/Quantifiers.bpl.expect | 20 + Test/test2/SelectiveChecking.bpl | 2 + Test/test2/SelectiveChecking.bpl.expect | 16 + Test/test2/Structured.bpl | 2 + Test/test2/Structured.bpl.expect | 20 + Test/test2/Timeouts0.bpl | 2 + Test/test2/Timeouts0.bpl.expect | 47 ++ Test/test2/TypeEncodingM.bpl | 2 + Test/test2/TypeEncodingM.bpl.expect | 5 + Test/test2/UpdateExpr.bpl | 2 + Test/test2/UpdateExpr.bpl.expect | 17 + Test/test2/Where.bpl | 2 + Test/test2/Where.bpl.expect | 37 ++ Test/test2/sk_hack.bpl | 2 + Test/test2/sk_hack.bpl.expect | 2 + Test/test2/strings-no-where.bpl | 2 + Test/test2/strings-no-where.bpl.expect | 19 + Test/test2/strings-where.bpl | 2 + Test/test2/strings-where.bpl.expect | 19 + 69 files changed, 837 insertions(+), 311 deletions(-) create mode 100644 Test/test2/Arrays.bpl.expect create mode 100644 Test/test2/AssumeEnsures.bpl.expect create mode 100644 Test/test2/AssumptionVariables0.bpl.expect create mode 100644 Test/test2/Axioms.bpl.expect create mode 100644 Test/test2/B.bpl.expect create mode 100644 Test/test2/Call.bpl.expect create mode 100644 Test/test2/ContractEvaluationOrder.bpl.expect create mode 100644 Test/test2/CutBackEdge.bpl.expect create mode 100644 Test/test2/Ensures.bpl.expect create mode 100644 Test/test2/False.bpl.expect create mode 100644 Test/test2/FormulaTerm.bpl.expect create mode 100644 Test/test2/FormulaTerm2.bpl.expect create mode 100644 Test/test2/FreeCall.bpl.expect create mode 100644 Test/test2/IfThenElse1.bpl.expect create mode 100644 Test/test2/Implies.bpl.expect create mode 100644 Test/test2/Lambda.bpl.expect create mode 100644 Test/test2/LambdaOldExpressions.bpl.expect create mode 100644 Test/test2/LambdaPoly.bpl.expect create mode 100644 Test/test2/LoopInvAssume.bpl.expect create mode 100644 Test/test2/NeverPattern.bpl.expect create mode 100644 Test/test2/NullaryMaps.bpl.expect create mode 100644 Test/test2/Old.bpl.expect create mode 100644 Test/test2/OldIllegal.bpl.expect create mode 100644 Test/test2/Passification.bpl.expect create mode 100644 Test/test2/Quantifiers.bpl.expect create mode 100644 Test/test2/SelectiveChecking.bpl.expect create mode 100644 Test/test2/Structured.bpl.expect create mode 100644 Test/test2/Timeouts0.bpl.expect create mode 100644 Test/test2/TypeEncodingM.bpl.expect create mode 100644 Test/test2/UpdateExpr.bpl.expect create mode 100644 Test/test2/Where.bpl.expect create mode 100644 Test/test2/sk_hack.bpl.expect create mode 100644 Test/test2/strings-no-where.bpl.expect create mode 100644 Test/test2/strings-where.bpl.expect diff --git a/Test/test2/Answer b/Test/test2/Answer index 898655b1..5d446e64 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -1,41 +1,41 @@ -------------------- FormulaTerm.bpl -------------------- -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. +FormulaTerm.bpl(12,3): Error BP5003: A postcondition might not hold on this return path. +FormulaTerm.bpl(6,3): Related location: This is the postcondition that might not hold. Execution trace: - FormulaTerm.bpl(8,1): start + FormulaTerm.bpl(10,1): start Boogie program verifier finished with 11 verified, 1 error -------------------- FormulaTerm2.bpl -------------------- -FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold. +FormulaTerm2.bpl(41,5): Error BP5001: This assertion might not hold. Execution trace: - FormulaTerm2.bpl(36,3): start -FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold. + FormulaTerm2.bpl(38,3): start +FormulaTerm2.bpl(49,5): Error BP5001: This assertion might not hold. Execution trace: - FormulaTerm2.bpl(45,3): start + FormulaTerm2.bpl(47,3): start Boogie program verifier finished with 2 verified, 2 errors -------------------- Passification.bpl -------------------- -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. +Passification.bpl(46,3): Error BP5003: A postcondition might not hold on this return path. +Passification.bpl(38,3): Related location: This is the postcondition that might not hold. Execution trace: - Passification.bpl(39,1): A -Passification.bpl(116,3): Error BP5001: This assertion might not hold. + Passification.bpl(41,1): A +Passification.bpl(118,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(151,3): Error BP5001: This assertion might not hold. + Passification.bpl(108,1): L0 + Passification.bpl(113,1): L1 + Passification.bpl(117,1): L2 +Passification.bpl(153,3): Error BP5001: This assertion might not hold. Execution trace: - Passification.bpl(144,1): L0 - Passification.bpl(150,1): L2 -Passification.bpl(165,3): Error BP5001: This assertion might not hold. + Passification.bpl(146,1): L0 + Passification.bpl(152,1): L2 +Passification.bpl(167,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(160,1): L0 + Passification.bpl(163,1): L1 + Passification.bpl(166,1): L2 Boogie program verifier finished with 7 verified, 4 errors @@ -44,121 +44,121 @@ 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 on this return path. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Ensures.bpl(32,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,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 on this return path. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. + Ensures.bpl(30,3): start +Ensures.bpl(37,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,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 on this return path. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. + Ensures.bpl(36,3): start +Ensures.bpl(43,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,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 on this return path. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. + Ensures.bpl(41,3): start +Ensures.bpl(49,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,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 on this return path. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. + Ensures.bpl(47,3): start +Ensures.bpl(74,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. Execution trace: - Ensures.bpl(70,3): start + Ensures.bpl(72,3): start Boogie program verifier finished with 5 verified, 5 errors -------------------- Old.bpl -------------------- -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. +Old.bpl(31,5): Error BP5003: A postcondition might not hold on this return path. +Old.bpl(28,3): Related location: This is the postcondition that might not hold. Execution trace: - Old.bpl(28,3): start + Old.bpl(30,3): start Boogie program verifier finished with 7 verified, 1 error -------------------- OldIllegal.bpl -------------------- -OldIllegal.bpl(7,11): Error: old expressions allowed only in two-state contexts -OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts +OldIllegal.bpl(9,11): Error: old expressions allowed only in two-state contexts +OldIllegal.bpl(16,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 on this return path. -Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. +Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(40,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 on this return path. -Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. + Arrays.bpl(44,3): start +Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(121,3): Related location: This is the postcondition that might not hold. Execution trace: - Arrays.bpl(123,3): start + Arrays.bpl(125,3): start Boogie program verifier finished with 8 verified, 2 errors -------------------- Axioms.bpl -------------------- -Axioms.bpl(19,5): Error BP5001: This assertion might not hold. +Axioms.bpl(21,5): Error BP5001: This assertion might not hold. Execution trace: - Axioms.bpl(18,3): start + Axioms.bpl(20,3): start Boogie program verifier finished with 2 verified, 1 error -------------------- Quantifiers.bpl -------------------- -Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold. +Quantifiers.bpl(22,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(19,3): start -Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold. + Quantifiers.bpl(21,3): start +Quantifiers.bpl(45,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(42,3): start -Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold. + Quantifiers.bpl(44,3): start +Quantifiers.bpl(67,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(64,3): start -Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold. + Quantifiers.bpl(66,3): start +Quantifiers.bpl(75,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(71,3): start -Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold. + Quantifiers.bpl(73,3): start +Quantifiers.bpl(127,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(124,3): start -Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold. + Quantifiers.bpl(126,3): start +Quantifiers.bpl(152,5): Error BP5001: This assertion might not hold. Execution trace: - Quantifiers.bpl(149,3): start + Quantifiers.bpl(151,3): start Boogie program verifier finished with 8 verified, 6 errors -------------------- Call.bpl -------------------- -Call.bpl(13,5): Error BP5001: This assertion might not hold. +Call.bpl(15,5): Error BP5001: This assertion might not hold. Execution trace: - Call.bpl(9,3): entry -Call.bpl(46,5): Error BP5001: This assertion might not hold. + Call.bpl(11,3): entry +Call.bpl(48,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 on this return path. -Call.bpl(20,3): Related location: This is the postcondition that might not hold. + Call.bpl(47,3): start +Call.bpl(57,5): Error BP5003: A postcondition might not hold on this return path. +Call.bpl(22,3): Related location: This is the postcondition that might not hold. Execution trace: - Call.bpl(53,3): start + Call.bpl(55,3): start Boogie program verifier finished with 2 verified, 3 errors -------------------- AssumeEnsures.bpl -------------------- -AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold. +AssumeEnsures.bpl(30,9): Error BP5001: This assertion might not hold. Execution trace: - AssumeEnsures.bpl(26,5): entry -AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold. + AssumeEnsures.bpl(28,5): entry +AssumeEnsures.bpl(49,9): Error BP5001: This assertion might not hold. Execution trace: - AssumeEnsures.bpl(46,5): entry -AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold. + AssumeEnsures.bpl(48,5): entry +AssumeEnsures.bpl(64,9): Error BP5001: This assertion might not hold. Execution trace: - AssumeEnsures.bpl(60,5): entry + AssumeEnsures.bpl(62,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. +CutBackEdge.bpl(12,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(20,5): Error BP5004: This loop invariant might not hold on entry. + CutBackEdge.bpl(7,3): entry + CutBackEdge.bpl(11,3): block850 +CutBackEdge.bpl(22,5): Error BP5004: This loop invariant might not hold on entry. Execution trace: -CutBackEdge.bpl(26,5): Error BP5001: This assertion might not hold. +CutBackEdge.bpl(28,5): Error BP5001: This assertion might not hold. Execution trace: - CutBackEdge.bpl(25,3): L -CutBackEdge.bpl(38,5): Error BP5004: This loop invariant might not hold on entry. + CutBackEdge.bpl(27,3): L +CutBackEdge.bpl(40,5): Error BP5004: This loop invariant might not hold on entry. Execution trace: Boogie program verifier finished with 1 verified, 4 errors @@ -168,310 +168,310 @@ Boogie program verifier finished with 1 verified, 4 errors Boogie program verifier finished with 2 verified, 0 errors -------------------- LoopInvAssume.bpl -------------------- -LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold. +LoopInvAssume.bpl(20,7): Error BP5001: This assertion might not hold. Execution trace: - LoopInvAssume.bpl(8,4): entry - LoopInvAssume.bpl(16,4): exit + LoopInvAssume.bpl(10,4): entry + LoopInvAssume.bpl(18,4): exit Boogie program verifier finished with 0 verified, 1 error -------------------- strings-no-where.bpl -------------------- -strings-no-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) -strings-no-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-no-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) -strings-no-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-no-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-no-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) -strings-no-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-no-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-no-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-no-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-no-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == -strings-no-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) -strings-no-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-no-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-no-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-no-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-no-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator == 18 type checking errors detected in strings-no-where.bpl -------------------- strings-where.bpl -------------------- -strings-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) -strings-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) -strings-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) -strings-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) -strings-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) -strings-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == -strings-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) -strings-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator == 18 type checking errors detected in strings-where.bpl -------------------- Structured.bpl -------------------- -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. +Structured.bpl(254,14): Error BP5003: A postcondition might not hold on this return path. +Structured.bpl(245,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,14): anon9_Then -Structured.bpl(303,3): Error BP5001: This assertion might not hold. + Structured.bpl(246,5): anon0 + Structured.bpl(248,5): anon6_LoopBody + Structured.bpl(249,7): anon7_LoopBody + Structured.bpl(250,11): anon8_Then + Structured.bpl(254,14): anon9_Then +Structured.bpl(305,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(311,7): Error BP5001: This assertion might not hold. + Structured.bpl(301,5): anon0 + Structured.bpl(302,3): anon3_Else + Structured.bpl(305,3): anon2 +Structured.bpl(313,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(310,3): anon0 + Structured.bpl(310,3): anon1_Then + Structured.bpl(311,5): A Boogie program verifier finished with 16 verified, 3 errors -------------------- Where.bpl -------------------- -Where.bpl(8,3): Error BP5001: This assertion might not hold. +Where.bpl(10,3): Error BP5001: This assertion might not hold. Execution trace: - Where.bpl(6,3): anon0 -Where.bpl(22,3): Error BP5001: This assertion might not hold. + Where.bpl(8,3): anon0 +Where.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - Where.bpl(16,5): anon0 -Where.bpl(32,3): Error BP5001: This assertion might not hold. + Where.bpl(18,5): anon0 +Where.bpl(34,3): Error BP5001: This assertion might not hold. Execution trace: - Where.bpl(30,3): anon0 -Where.bpl(44,3): Error BP5001: This assertion might not hold. + Where.bpl(32,3): anon0 +Where.bpl(46,3): Error BP5001: This assertion might not hold. Execution trace: - Where.bpl(40,5): anon0 -Where.bpl(57,3): Error BP5001: This assertion might not hold. + Where.bpl(42,5): anon0 +Where.bpl(59,3): Error BP5001: This assertion might not hold. Execution trace: - Where.bpl(52,3): anon0 -Where.bpl(111,3): Error BP5001: This assertion might not hold. + Where.bpl(54,3): anon0 +Where.bpl(113,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(128,3): Error BP5001: This assertion might not hold. + Where.bpl(104,5): anon0 + Where.bpl(106,3): anon3_LoopHead + Where.bpl(106,3): anon3_LoopDone +Where.bpl(130,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(145,3): Error BP5001: This assertion might not hold. + Where.bpl(123,5): anon0 + Where.bpl(124,3): anon3_LoopHead + Where.bpl(124,3): anon3_LoopDone +Where.bpl(147,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(162,3): Error BP5001: This assertion might not hold. + Where.bpl(140,5): anon0 + Where.bpl(141,3): anon3_LoopHead + Where.bpl(141,3): anon3_LoopDone +Where.bpl(164,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(157,5): anon0 + Where.bpl(158,3): anon3_LoopHead + Where.bpl(158,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. +UpdateExpr.bpl(16,3): Error BP5001: This assertion might not hold. Execution trace: - UpdateExpr.bpl(14,3): anon0 -UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold. + UpdateExpr.bpl(16,3): anon0 +UpdateExpr.bpl(21,3): Error BP5001: This assertion might not hold. Execution trace: - UpdateExpr.bpl(19,3): anon0 -UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold. + UpdateExpr.bpl(21,3): anon0 +UpdateExpr.bpl(34,3): Error BP5001: This assertion might not hold. Execution trace: - UpdateExpr.bpl(32,3): anon0 -UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold. + UpdateExpr.bpl(34,3): anon0 +UpdateExpr.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - UpdateExpr.bpl(38,3): anon0 -UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold. + UpdateExpr.bpl(40,3): anon0 +UpdateExpr.bpl(54,3): Error BP5001: This assertion might not hold. Execution trace: - UpdateExpr.bpl(51,5): anon0 + UpdateExpr.bpl(53,5): anon0 Boogie program verifier finished with 5 verified, 5 errors -------------------- NeverPattern.bpl -------------------- -NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold. +NeverPattern.bpl(18,3): Error BP5001: This assertion might not hold. Execution trace: - NeverPattern.bpl(15,3): anon0 -NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold. + NeverPattern.bpl(17,3): anon0 +NeverPattern.bpl(24,3): Error BP5001: This assertion might not hold. Execution trace: - NeverPattern.bpl(21,3): anon0 -NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold. + NeverPattern.bpl(23,3): anon0 +NeverPattern.bpl(30,3): Error BP5001: This assertion might not hold. Execution trace: - NeverPattern.bpl(27,3): anon0 + NeverPattern.bpl(29,3): anon0 Boogie program verifier finished with 2 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(30,3): Error BP5001: This assertion might not hold. Execution trace: - NullaryMaps.bpl(28,3): anon0 -NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold. + NullaryMaps.bpl(30,3): anon0 +NullaryMaps.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(30,3): anon0 +NullaryMaps.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace: - NullaryMaps.bpl(36,3): anon0 + NullaryMaps.bpl(38,3): anon0 Boogie program verifier finished with 2 verified, 3 errors -------------------- Implies.bpl -------------------- -Implies.bpl(12,3): Error BP5001: This assertion might not hold. +Implies.bpl(14,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(11,3): anon0 -Implies.bpl(15,3): Error BP5001: This assertion might not hold. + Implies.bpl(13,3): anon0 +Implies.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(11,3): anon0 -Implies.bpl(19,3): Error BP5001: This assertion might not hold. + Implies.bpl(13,3): anon0 +Implies.bpl(21,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(19,3): anon0 -Implies.bpl(24,3): Error BP5001: This assertion might not hold. + Implies.bpl(21,3): anon0 +Implies.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(24,3): anon0 -Implies.bpl(25,3): Error BP5001: This assertion might not hold. + Implies.bpl(26,3): anon0 +Implies.bpl(27,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(24,3): anon0 -Implies.bpl(29,3): Error BP5001: This assertion might not hold. + Implies.bpl(26,3): anon0 +Implies.bpl(31,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(29,3): anon0 -Implies.bpl(34,3): Error BP5001: This assertion might not hold. + Implies.bpl(31,3): anon0 +Implies.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(34,3): anon0 -Implies.bpl(35,3): Error BP5001: This assertion might not hold. + Implies.bpl(36,3): anon0 +Implies.bpl(37,3): Error BP5001: This assertion might not hold. Execution trace: - Implies.bpl(34,3): anon0 + Implies.bpl(36,3): anon0 Boogie program verifier finished with 0 verified, 8 errors -------------------- IfThenElse1.bpl -------------------- -IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold. +IfThenElse1.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - IfThenElse1.bpl(26,3): anon0 -IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold. + IfThenElse1.bpl(28,3): anon0 +IfThenElse1.bpl(35,3): Error BP5001: This assertion might not hold. Execution trace: - IfThenElse1.bpl(33,3): anon0 + IfThenElse1.bpl(35,3): anon0 Boogie program verifier finished with 2 verified, 2 errors -------------------- Lambda.bpl -------------------- -Lambda.bpl(37,3): Error BP5001: This assertion might not hold. +Lambda.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - Lambda.bpl(36,5): anon0 -Lambda.bpl(38,3): Error BP5001: This assertion might not hold. + Lambda.bpl(38,5): anon0 +Lambda.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - Lambda.bpl(36,5): anon0 + Lambda.bpl(38,5): anon0 Boogie program verifier finished with 6 verified, 2 errors -------------------- LambdaPoly.bpl -------------------- -LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold. +LambdaPoly.bpl(30,5): Error BP5001: This assertion might not hold. Execution trace: - LambdaPoly.bpl(24,5): anon0 - LambdaPoly.bpl(27,5): anon4_Then -LambdaPoly.bpl(31,5): Error BP5001: This assertion might not hold. + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(29,5): anon4_Then +LambdaPoly.bpl(33,5): Error BP5001: This assertion might not hold. Execution trace: - LambdaPoly.bpl(24,5): anon0 - LambdaPoly.bpl(30,5): anon5_Then -LambdaPoly.bpl(36,5): Error BP5001: This assertion might not hold. + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(32,5): anon5_Then +LambdaPoly.bpl(38,5): Error BP5001: This assertion might not hold. Execution trace: - LambdaPoly.bpl(24,5): anon0 - LambdaPoly.bpl(34,5): anon5_Else + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(36,5): anon5_Else Boogie program verifier finished with 1 verified, 3 errors -------------------- LambdaOldExpressions.bpl -------------------- -LambdaOldExpressions.bpl(27,1): Error BP5003: A postcondition might not hold on this return path. -LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that might not hold. +LambdaOldExpressions.bpl(29,1): Error BP5003: A postcondition might not hold on this return path. +LambdaOldExpressions.bpl(23,3): Related location: This is the postcondition that might not hold. Execution trace: - LambdaOldExpressions.bpl(25,7): anon0 + LambdaOldExpressions.bpl(27,7): anon0 Boogie program verifier finished with 4 verified, 1 error -------------------- SelectiveChecking.bpl -------------------- -SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold. -Execution trace: - SelectiveChecking.bpl(15,3): anon0 -SelectiveChecking.bpl(30,3): Error BP5001: This assertion might not hold. +SelectiveChecking.bpl(19,3): Error BP5001: This assertion might not hold. Execution trace: - SelectiveChecking.bpl(24,3): anon0 - SelectiveChecking.bpl(27,5): anon3_Then - SelectiveChecking.bpl(30,3): anon2 -SelectiveChecking.bpl(37,3): Error BP5001: This assertion might not hold. + SelectiveChecking.bpl(17,3): anon0 +SelectiveChecking.bpl(32,3): Error BP5001: This assertion might not hold. Execution trace: - SelectiveChecking.bpl(37,3): anon0 + SelectiveChecking.bpl(26,3): anon0 + SelectiveChecking.bpl(29,5): anon3_Then + SelectiveChecking.bpl(32,3): anon2 SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - SelectiveChecking.bpl(37,3): anon0 + SelectiveChecking.bpl(39,3): anon0 +SelectiveChecking.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + SelectiveChecking.bpl(39,3): anon0 Boogie program verifier finished with 1 verified, 4 errors -------------------- FreeCall.bpl -------------------- -FreeCall.bpl(37,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(39,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(10,3): Related location: This is the precondition that might not hold. +Execution trace: + FreeCall.bpl(39,5): anon0 +FreeCall.bpl(44,5): Error BP5002: A precondition for this call might not hold. FreeCall.bpl(8,3): Related location: This is the precondition that might not hold. Execution trace: - FreeCall.bpl(37,5): anon0 -FreeCall.bpl(42,5): Error BP5002: A precondition for this call might not hold. -FreeCall.bpl(6,3): Related location: This is the precondition that might not hold. + FreeCall.bpl(44,5): anon0 +FreeCall.bpl(61,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(18,3): Related location: This is the precondition that might not hold. Execution trace: - FreeCall.bpl(42,5): anon0 -FreeCall.bpl(59,5): Error BP5002: A precondition for this call might not hold. + FreeCall.bpl(61,5): anon0 +FreeCall.bpl(68,5): Error BP5002: A precondition for this call might not hold. FreeCall.bpl(16,3): Related location: This is the precondition that might not hold. Execution trace: - FreeCall.bpl(59,5): anon0 -FreeCall.bpl(66,5): Error BP5002: A precondition for this call might not hold. -FreeCall.bpl(14,3): Related location: This is the precondition that might not hold. -Execution trace: - FreeCall.bpl(66,5): anon0 + FreeCall.bpl(68,5): anon0 Boogie program verifier finished with 7 verified, 4 errors -------------------- AssumptionVariables0.bpl -------------------- -AssumptionVariables0.bpl(15,5): Error BP5001: This assertion might not hold. +AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold. Execution trace: - AssumptionVariables0.bpl(13,8): anon0 -AssumptionVariables0.bpl(25,5): Error BP5001: This assertion might not hold. + AssumptionVariables0.bpl(15,8): anon0 +AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold. Execution trace: - AssumptionVariables0.bpl(23,5): anon0 -AssumptionVariables0.bpl(37,5): Error BP5001: This assertion might not hold. + AssumptionVariables0.bpl(25,5): anon0 +AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold. Execution trace: - AssumptionVariables0.bpl(35,8): anon0 + AssumptionVariables0.bpl(37,8): anon0 Boogie program verifier finished with 1 verified, 3 errors -------------------- Arrays.bpl /typeEncoding:m -------------------- -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. +Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(40,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 on this return path. -Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. + Arrays.bpl(44,3): start +Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(121,3): Related location: This is the postcondition that might not hold. Execution trace: - Arrays.bpl(123,3): start + Arrays.bpl(125,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. +Lambda.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - Lambda.bpl(36,5): anon0 -Lambda.bpl(38,3): Error BP5001: This assertion might not hold. + Lambda.bpl(38,5): anon0 +Lambda.bpl(40,3): Error BP5001: This assertion might not hold. Execution trace: - Lambda.bpl(36,5): anon0 + Lambda.bpl(38,5): anon0 Boogie program verifier finished with 6 verified, 2 errors -------------------- TypeEncodingM.bpl /typeEncoding:m -------------------- -TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold. +TypeEncodingM.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - TypeEncodingM.bpl(11,9): anon0 + TypeEncodingM.bpl(13,9): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- sk_hack.bpl -------------------- @@ -479,65 +479,65 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors -------------------- ContractEvaluationOrder.bpl -------------------- -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. +ContractEvaluationOrder.bpl(10,1): Error BP5003: A postcondition might not hold on this return path. +ContractEvaluationOrder.bpl(5,3): Related location: This is the postcondition that might not hold. Execution trace: - ContractEvaluationOrder.bpl(7,5): anon0 -ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold. + ContractEvaluationOrder.bpl(9,5): anon0 +ContractEvaluationOrder.bpl(17,3): Error BP5001: This assertion might not hold. Execution trace: - 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. + ContractEvaluationOrder.bpl(14,5): anon0 +ContractEvaluationOrder.bpl(26,3): Error BP5002: A precondition for this call might not hold. +ContractEvaluationOrder.bpl(32,3): Related location: This is the precondition that might not hold. Execution trace: - ContractEvaluationOrder.bpl(23,5): anon0 + ContractEvaluationOrder.bpl(25,5): anon0 Boogie program verifier finished with 1 verified, 3 errors -------------------- Timeouts0.bpl -------------------- -Timeouts0.bpl(19,5): Error BP5003: A postcondition might not hold on this return path. -Timeouts0.bpl(4,3): Related location: This is the postcondition that might not hold. -Execution trace: - Timeouts0.bpl(8,7): anon0 - Timeouts0.bpl(10,5): anon4_LoopHead - Timeouts0.bpl(10,5): anon4_LoopDone - Timeouts0.bpl(19,5): anon5_LoopHead - Timeouts0.bpl(19,5): anon5_LoopDone -Timeouts0.bpl(21,7): Error BP5005: This loop invariant might not be maintained by the loop. -Execution trace: - Timeouts0.bpl(8,7): anon0 - Timeouts0.bpl(10,5): anon4_LoopHead - Timeouts0.bpl(10,5): anon4_LoopDone - Timeouts0.bpl(19,5): anon5_LoopHead - Timeouts0.bpl(23,11): anon5_LoopBody -Timeouts0.bpl(48,5): Error BP5003: A postcondition might not hold on this return path. -Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold. -Execution trace: - Timeouts0.bpl(37,7): anon0 - Timeouts0.bpl(39,5): anon4_LoopHead - Timeouts0.bpl(39,5): anon4_LoopDone - Timeouts0.bpl(48,5): anon5_LoopHead - Timeouts0.bpl(48,5): anon5_LoopDone -Timeouts0.bpl(50,7): Error BP5005: This loop invariant might not be maintained by the loop. -Execution trace: - Timeouts0.bpl(37,7): anon0 - Timeouts0.bpl(39,5): anon4_LoopHead - Timeouts0.bpl(39,5): anon4_LoopDone - Timeouts0.bpl(48,5): anon5_LoopHead - Timeouts0.bpl(52,11): anon5_LoopBody -Timeouts0.bpl(77,5): Error BP5003: A postcondition might not hold on this return path. -Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold. -Execution trace: - Timeouts0.bpl(66,7): anon0 - Timeouts0.bpl(68,5): anon4_LoopHead - Timeouts0.bpl(68,5): anon4_LoopDone - Timeouts0.bpl(77,5): anon5_LoopHead - Timeouts0.bpl(77,5): anon5_LoopDone -Timeouts0.bpl(79,7): Error BP5005: This loop invariant might not be maintained by the loop. -Execution trace: - Timeouts0.bpl(66,7): anon0 - Timeouts0.bpl(68,5): anon4_LoopHead - Timeouts0.bpl(68,5): anon4_LoopDone - Timeouts0.bpl(77,5): anon5_LoopHead - Timeouts0.bpl(81,11): anon5_LoopBody +Timeouts0.bpl(21,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(6,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(10,7): anon0 + Timeouts0.bpl(12,5): anon4_LoopHead + Timeouts0.bpl(12,5): anon4_LoopDone + Timeouts0.bpl(21,5): anon5_LoopHead + Timeouts0.bpl(21,5): anon5_LoopDone +Timeouts0.bpl(23,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(10,7): anon0 + Timeouts0.bpl(12,5): anon4_LoopHead + Timeouts0.bpl(12,5): anon4_LoopDone + Timeouts0.bpl(21,5): anon5_LoopHead + Timeouts0.bpl(25,11): anon5_LoopBody +Timeouts0.bpl(50,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(33,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(39,7): anon0 + Timeouts0.bpl(41,5): anon4_LoopHead + Timeouts0.bpl(41,5): anon4_LoopDone + Timeouts0.bpl(50,5): anon5_LoopHead + Timeouts0.bpl(50,5): anon5_LoopDone +Timeouts0.bpl(52,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(39,7): anon0 + Timeouts0.bpl(41,5): anon4_LoopHead + Timeouts0.bpl(41,5): anon4_LoopDone + Timeouts0.bpl(50,5): anon5_LoopHead + Timeouts0.bpl(54,11): anon5_LoopBody +Timeouts0.bpl(79,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(62,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(68,7): anon0 + Timeouts0.bpl(70,5): anon4_LoopHead + Timeouts0.bpl(70,5): anon4_LoopDone + Timeouts0.bpl(79,5): anon5_LoopHead + Timeouts0.bpl(79,5): anon5_LoopDone +Timeouts0.bpl(81,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(68,7): anon0 + Timeouts0.bpl(70,5): anon4_LoopHead + Timeouts0.bpl(70,5): anon4_LoopDone + Timeouts0.bpl(79,5): anon5_LoopHead + Timeouts0.bpl(83,11): anon5_LoopBody Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test2/Arrays.bpl b/Test/test2/Arrays.bpl index d0f712c9..f153b599 100644 --- a/Test/test2/Arrays.bpl +++ b/Test/test2/Arrays.bpl @@ -1,3 +1,7 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t +// RUN: %boogie -noinfer -typeEncoding:m %s > %t +// RUN: %diff %s.expect %t // -------------------- 1-dimensional arrays -------------------- var A: [ref]int; diff --git a/Test/test2/Arrays.bpl.expect b/Test/test2/Arrays.bpl.expect new file mode 100644 index 00000000..34804dc0 --- /dev/null +++ b/Test/test2/Arrays.bpl.expect @@ -0,0 +1,10 @@ +Arrays.bpl(50,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(42,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(46,3): start +Arrays.bpl(131,5): Error BP5003: A postcondition might not hold on this return path. +Arrays.bpl(123,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(127,3): start + +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl index 901c06c8..9c19e5bc 100644 --- a/Test/test2/AssumeEnsures.bpl +++ b/Test/test2/AssumeEnsures.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t var g: int; procedure Foo() returns (); diff --git a/Test/test2/AssumeEnsures.bpl.expect b/Test/test2/AssumeEnsures.bpl.expect new file mode 100644 index 00000000..7a65cace --- /dev/null +++ b/Test/test2/AssumeEnsures.bpl.expect @@ -0,0 +1,11 @@ +AssumeEnsures.bpl(30,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(28,5): entry +AssumeEnsures.bpl(49,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(48,5): entry +AssumeEnsures.bpl(64,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(62,5): entry + +Boogie program verifier finished with 4 verified, 3 errors diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl index 96537c0d..e1800d3d 100644 --- a/Test/test2/AssumptionVariables0.bpl +++ b/Test/test2/AssumptionVariables0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure Test0() { var {:assumption} a0: bool; diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect new file mode 100644 index 00000000..54ddb2a9 --- /dev/null +++ b/Test/test2/AssumptionVariables0.bpl.expect @@ -0,0 +1,11 @@ +AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold. +Execution trace: + AssumptionVariables0.bpl(15,8): anon0 +AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold. +Execution trace: + AssumptionVariables0.bpl(25,5): anon0 +AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold. +Execution trace: + AssumptionVariables0.bpl(37,8): anon0 + +Boogie program verifier finished with 1 verified, 3 errors diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl index 4fe7a8a7..0da46116 100644 --- a/Test/test2/Axioms.bpl +++ b/Test/test2/Axioms.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t const Seven: int; axiom Seven == 7; diff --git a/Test/test2/Axioms.bpl.expect b/Test/test2/Axioms.bpl.expect new file mode 100644 index 00000000..2557ee13 --- /dev/null +++ b/Test/test2/Axioms.bpl.expect @@ -0,0 +1,5 @@ +Axioms.bpl(21,5): Error BP5001: This assertion might not hold. +Execution trace: + Axioms.bpl(20,3): start + +Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl index 553d5002..f68dbb26 100644 --- a/Test/test2/B.bpl +++ b/Test/test2/B.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // ----------- BEGIN PRELUDE var Heap: [ref, name]int; diff --git a/Test/test2/B.bpl.expect b/Test/test2/B.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/test2/B.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/test2/Call.bpl b/Test/test2/Call.bpl index c1de1e71..02902b0a 100644 --- a/Test/test2/Call.bpl +++ b/Test/test2/Call.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure Bar() returns (barresult: ref); procedure Foo(); diff --git a/Test/test2/Call.bpl.expect b/Test/test2/Call.bpl.expect new file mode 100644 index 00000000..934b3ac5 --- /dev/null +++ b/Test/test2/Call.bpl.expect @@ -0,0 +1,12 @@ +Call.bpl(15,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(11,3): entry +Call.bpl(48,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(47,3): start +Call.bpl(57,5): Error BP5003: A postcondition might not hold on this return path. +Call.bpl(22,3): Related location: This is the postcondition that might not hold. +Execution trace: + Call.bpl(55,3): start + +Boogie program verifier finished with 2 verified, 3 errors diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl index 3eab4bda..445b84c6 100644 --- a/Test/test2/ContractEvaluationOrder.bpl +++ b/Test/test2/ContractEvaluationOrder.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t procedure P() returns (x, y: int) ensures x == y; // ensured by the body ensures x == 0; // error: not ensured by the body diff --git a/Test/test2/ContractEvaluationOrder.bpl.expect b/Test/test2/ContractEvaluationOrder.bpl.expect new file mode 100644 index 00000000..4bab4b21 --- /dev/null +++ b/Test/test2/ContractEvaluationOrder.bpl.expect @@ -0,0 +1,13 @@ +ContractEvaluationOrder.bpl(10,1): Error BP5003: A postcondition might not hold on this return path. +ContractEvaluationOrder.bpl(5,3): Related location: This is the postcondition that might not hold. +Execution trace: + ContractEvaluationOrder.bpl(9,5): anon0 +ContractEvaluationOrder.bpl(17,3): Error BP5001: This assertion might not hold. +Execution trace: + ContractEvaluationOrder.bpl(14,5): anon0 +ContractEvaluationOrder.bpl(26,3): Error BP5002: A precondition for this call might not hold. +ContractEvaluationOrder.bpl(32,3): Related location: This is the precondition that might not hold. +Execution trace: + ContractEvaluationOrder.bpl(25,5): anon0 + +Boogie program verifier finished with 1 verified, 3 errors diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl index 7294d0f9..c1d08216 100644 --- a/Test/test2/CutBackEdge.bpl +++ b/Test/test2/CutBackEdge.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure Test() { var i: int; diff --git a/Test/test2/CutBackEdge.bpl.expect b/Test/test2/CutBackEdge.bpl.expect new file mode 100644 index 00000000..90719e35 --- /dev/null +++ b/Test/test2/CutBackEdge.bpl.expect @@ -0,0 +1,13 @@ +CutBackEdge.bpl(12,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + CutBackEdge.bpl(7,3): entry + CutBackEdge.bpl(11,3): block850 +CutBackEdge.bpl(22,5): Error BP5004: This loop invariant might not hold on entry. +Execution trace: +CutBackEdge.bpl(28,5): Error BP5001: This assertion might not hold. +Execution trace: + CutBackEdge.bpl(27,3): L +CutBackEdge.bpl(40,5): Error BP5004: This loop invariant might not hold on entry. +Execution trace: + +Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/test2/Ensures.bpl b/Test/test2/Ensures.bpl index 4e36c108..8996d100 100644 --- a/Test/test2/Ensures.bpl +++ b/Test/test2/Ensures.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t var H: [ref,name]int; var that: ref; diff --git a/Test/test2/Ensures.bpl.expect b/Test/test2/Ensures.bpl.expect new file mode 100644 index 00000000..28917250 --- /dev/null +++ b/Test/test2/Ensures.bpl.expect @@ -0,0 +1,22 @@ +Ensures.bpl(32,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(30,3): start +Ensures.bpl(37,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(36,3): start +Ensures.bpl(43,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(41,3): start +Ensures.bpl(49,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(47,3): start +Ensures.bpl(74,5): Error BP5003: A postcondition might not hold on this return path. +Ensures.bpl(21,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(72,3): start + +Boogie program verifier finished with 5 verified, 5 errors diff --git a/Test/test2/False.bpl b/Test/test2/False.bpl index 3fe14865..5399b024 100644 --- a/Test/test2/False.bpl +++ b/Test/test2/False.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure Test1() { entry: diff --git a/Test/test2/False.bpl.expect b/Test/test2/False.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/test2/False.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/test2/FormulaTerm.bpl b/Test/test2/FormulaTerm.bpl index e14707cb..b36f971b 100644 --- a/Test/test2/FormulaTerm.bpl +++ b/Test/test2/FormulaTerm.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // Test formula-term distinction in Simplify procedure plus(x: int, y: int) returns (z: int); diff --git a/Test/test2/FormulaTerm.bpl.expect b/Test/test2/FormulaTerm.bpl.expect new file mode 100644 index 00000000..70fe60b3 --- /dev/null +++ b/Test/test2/FormulaTerm.bpl.expect @@ -0,0 +1,6 @@ +FormulaTerm.bpl(12,3): Error BP5003: A postcondition might not hold on this return path. +FormulaTerm.bpl(6,3): Related location: This is the postcondition that might not hold. +Execution trace: + FormulaTerm.bpl(10,1): start + +Boogie program verifier finished with 11 verified, 1 error diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl index 6c5e4bf3..881a6222 100644 --- a/Test/test2/FormulaTerm2.bpl +++ b/Test/test2/FormulaTerm2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // This file has been created to test some of the formula/term issues in Zap. // However, the test harness does not specify any particular prover to be used, // since these tests should pass regardless of which prover is used. diff --git a/Test/test2/FormulaTerm2.bpl.expect b/Test/test2/FormulaTerm2.bpl.expect new file mode 100644 index 00000000..aa959a1d --- /dev/null +++ b/Test/test2/FormulaTerm2.bpl.expect @@ -0,0 +1,8 @@ +FormulaTerm2.bpl(41,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(38,3): start +FormulaTerm2.bpl(49,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(47,3): start + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test2/FreeCall.bpl b/Test/test2/FreeCall.bpl index a873a4e6..aaaba3ac 100644 --- a/Test/test2/FreeCall.bpl +++ b/Test/test2/FreeCall.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // Test the implementation of free calls. These calls don't check the preconditions of the // called procedure in the caller. diff --git a/Test/test2/FreeCall.bpl.expect b/Test/test2/FreeCall.bpl.expect new file mode 100644 index 00000000..edcfee63 --- /dev/null +++ b/Test/test2/FreeCall.bpl.expect @@ -0,0 +1,18 @@ +FreeCall.bpl(39,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(10,3): Related location: This is the precondition that might not hold. +Execution trace: + FreeCall.bpl(39,5): anon0 +FreeCall.bpl(44,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(8,3): Related location: This is the precondition that might not hold. +Execution trace: + FreeCall.bpl(44,5): anon0 +FreeCall.bpl(61,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(18,3): Related location: This is the precondition that might not hold. +Execution trace: + FreeCall.bpl(61,5): anon0 +FreeCall.bpl(68,5): Error BP5002: A precondition for this call might not hold. +FreeCall.bpl(16,3): Related location: This is the precondition that might not hold. +Execution trace: + FreeCall.bpl(68,5): anon0 + +Boogie program verifier finished with 7 verified, 4 errors diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl index 8a867f50..4c79ce8b 100644 --- a/Test/test2/IfThenElse1.bpl +++ b/Test/test2/IfThenElse1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t type t1; procedure ok() diff --git a/Test/test2/IfThenElse1.bpl.expect b/Test/test2/IfThenElse1.bpl.expect new file mode 100644 index 00000000..48386461 --- /dev/null +++ b/Test/test2/IfThenElse1.bpl.expect @@ -0,0 +1,8 @@ +IfThenElse1.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + IfThenElse1.bpl(28,3): anon0 +IfThenElse1.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + IfThenElse1.bpl(35,3): anon0 + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test2/Implies.bpl b/Test/test2/Implies.bpl index f20b0450..05a3e5fe 100644 --- a/Test/test2/Implies.bpl +++ b/Test/test2/Implies.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t const a:bool; const b:bool; diff --git a/Test/test2/Implies.bpl.expect b/Test/test2/Implies.bpl.expect new file mode 100644 index 00000000..93e83ffd --- /dev/null +++ b/Test/test2/Implies.bpl.expect @@ -0,0 +1,26 @@ +Implies.bpl(14,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(13,3): anon0 +Implies.bpl(17,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(13,3): anon0 +Implies.bpl(21,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(21,3): anon0 +Implies.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(26,3): anon0 +Implies.bpl(27,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(26,3): anon0 +Implies.bpl(31,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(31,3): anon0 +Implies.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(36,3): anon0 +Implies.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(36,3): anon0 + +Boogie program verifier finished with 0 verified, 8 errors diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl index 68c83d43..cbcbd334 100644 --- a/Test/test2/Lambda.bpl +++ b/Test/test2/Lambda.bpl @@ -1,3 +1,7 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t +// RUN: %boogie -noinfer -typeEncoding:m %s > %t +// RUN: %diff %s.expect %t procedure foo() { var a: [int]int; diff --git a/Test/test2/Lambda.bpl.expect b/Test/test2/Lambda.bpl.expect new file mode 100644 index 00000000..d45375fa --- /dev/null +++ b/Test/test2/Lambda.bpl.expect @@ -0,0 +1,8 @@ +Lambda.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + Lambda.bpl(40,5): anon0 +Lambda.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + Lambda.bpl(40,5): anon0 + +Boogie program verifier finished with 6 verified, 2 errors diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl index 9f17245f..94a6e520 100644 --- a/Test/test2/LambdaOldExpressions.bpl +++ b/Test/test2/LambdaOldExpressions.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t var b: bool; diff --git a/Test/test2/LambdaOldExpressions.bpl.expect b/Test/test2/LambdaOldExpressions.bpl.expect new file mode 100644 index 00000000..1268eb7e --- /dev/null +++ b/Test/test2/LambdaOldExpressions.bpl.expect @@ -0,0 +1,6 @@ +LambdaOldExpressions.bpl(29,1): Error BP5003: A postcondition might not hold on this return path. +LambdaOldExpressions.bpl(23,3): Related location: This is the postcondition that might not hold. +Execution trace: + LambdaOldExpressions.bpl(27,7): anon0 + +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/test2/LambdaPoly.bpl b/Test/test2/LambdaPoly.bpl index 0fec0260..9a3fa16a 100644 --- a/Test/test2/LambdaPoly.bpl +++ b/Test/test2/LambdaPoly.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t type set a = [a]bool; function union(a:set T, b:set T) : set T; axiom (forall a,b:set T :: union(a,b) == (lambda x:T :: a[x] || b[x])); diff --git a/Test/test2/LambdaPoly.bpl.expect b/Test/test2/LambdaPoly.bpl.expect new file mode 100644 index 00000000..9d080e36 --- /dev/null +++ b/Test/test2/LambdaPoly.bpl.expect @@ -0,0 +1,14 @@ +LambdaPoly.bpl(30,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(29,5): anon4_Then +LambdaPoly.bpl(33,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(32,5): anon5_Then +LambdaPoly.bpl(38,5): Error BP5001: This assertion might not hold. +Execution trace: + LambdaPoly.bpl(26,5): anon0 + LambdaPoly.bpl(36,5): anon5_Else + +Boogie program verifier finished with 1 verified, 3 errors diff --git a/Test/test2/LoopInvAssume.bpl b/Test/test2/LoopInvAssume.bpl index 1304e668..ecbcdc7c 100644 --- a/Test/test2/LoopInvAssume.bpl +++ b/Test/test2/LoopInvAssume.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // Check that assumes in loop invariants are handled correctly var x : int; diff --git a/Test/test2/LoopInvAssume.bpl.expect b/Test/test2/LoopInvAssume.bpl.expect new file mode 100644 index 00000000..6fda9cf0 --- /dev/null +++ b/Test/test2/LoopInvAssume.bpl.expect @@ -0,0 +1,6 @@ +LoopInvAssume.bpl(20,7): Error BP5001: This assertion might not hold. +Execution trace: + LoopInvAssume.bpl(10,4): entry + LoopInvAssume.bpl(18,4): exit + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl index 1e0fed76..c859afe4 100644 --- a/Test/test2/NeverPattern.bpl +++ b/Test/test2/NeverPattern.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t function {:never_pattern true} f1(x:int) returns(int); function {:never_pattern false} f2(x:int) returns(int); function f3(x:int) returns(int); diff --git a/Test/test2/NeverPattern.bpl.expect b/Test/test2/NeverPattern.bpl.expect new file mode 100644 index 00000000..3ce334aa --- /dev/null +++ b/Test/test2/NeverPattern.bpl.expect @@ -0,0 +1,11 @@ +NeverPattern.bpl(18,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(17,3): anon0 +NeverPattern.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(23,3): anon0 +NeverPattern.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(29,3): anon0 + +Boogie program verifier finished with 2 verified, 3 errors diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl index 1bc18c41..ed08ec93 100644 --- a/Test/test2/NullaryMaps.bpl +++ b/Test/test2/NullaryMaps.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // aren't these cool! var m: []int; diff --git a/Test/test2/NullaryMaps.bpl.expect b/Test/test2/NullaryMaps.bpl.expect new file mode 100644 index 00000000..bb48b1d5 --- /dev/null +++ b/Test/test2/NullaryMaps.bpl.expect @@ -0,0 +1,11 @@ +NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(30,3): anon0 +NullaryMaps.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(30,3): anon0 +NullaryMaps.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(38,3): anon0 + +Boogie program verifier finished with 2 verified, 3 errors diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl index 00f798bc..99db9841 100644 --- a/Test/test2/Old.bpl +++ b/Test/test2/Old.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t var x: int; var y: int; diff --git a/Test/test2/Old.bpl.expect b/Test/test2/Old.bpl.expect new file mode 100644 index 00000000..ca98d32b --- /dev/null +++ b/Test/test2/Old.bpl.expect @@ -0,0 +1,6 @@ +Old.bpl(31,5): Error BP5003: A postcondition might not hold on this return path. +Old.bpl(28,3): Related location: This is the postcondition that might not hold. +Execution trace: + Old.bpl(30,3): start + +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/test2/OldIllegal.bpl b/Test/test2/OldIllegal.bpl index 342c5b19..d2defb25 100644 --- a/Test/test2/OldIllegal.bpl +++ b/Test/test2/OldIllegal.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // Test old appearing in illegal locations var Global0: int; diff --git a/Test/test2/OldIllegal.bpl.expect b/Test/test2/OldIllegal.bpl.expect new file mode 100644 index 00000000..6c5f8013 --- /dev/null +++ b/Test/test2/OldIllegal.bpl.expect @@ -0,0 +1,3 @@ +OldIllegal.bpl(9,11): Error: old expressions allowed only in two-state contexts +OldIllegal.bpl(16,23): Error: old expressions allowed only in two-state contexts +2 name resolution errors detected in OldIllegal.bpl diff --git a/Test/test2/Passification.bpl b/Test/test2/Passification.bpl index e13d3e49..521a9d59 100644 --- a/Test/test2/Passification.bpl +++ b/Test/test2/Passification.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // VC generation tests: passification procedure good0(x: int) returns (y: int, z: int) diff --git a/Test/test2/Passification.bpl.expect b/Test/test2/Passification.bpl.expect new file mode 100644 index 00000000..65880ca4 --- /dev/null +++ b/Test/test2/Passification.bpl.expect @@ -0,0 +1,20 @@ +Passification.bpl(46,3): Error BP5003: A postcondition might not hold on this return path. +Passification.bpl(38,3): Related location: This is the postcondition that might not hold. +Execution trace: + Passification.bpl(41,1): A +Passification.bpl(118,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(108,1): L0 + Passification.bpl(113,1): L1 + Passification.bpl(117,1): L2 +Passification.bpl(153,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(146,1): L0 + Passification.bpl(152,1): L2 +Passification.bpl(167,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(160,1): L0 + Passification.bpl(163,1): L1 + Passification.bpl(166,1): L2 + +Boogie program verifier finished with 7 verified, 4 errors diff --git a/Test/test2/Quantifiers.bpl b/Test/test2/Quantifiers.bpl index d368fe1f..e4a50c6b 100644 --- a/Test/test2/Quantifiers.bpl +++ b/Test/test2/Quantifiers.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t // ----------------------------------------------------------------------- single trigger function f(int, int) returns (int); diff --git a/Test/test2/Quantifiers.bpl.expect b/Test/test2/Quantifiers.bpl.expect new file mode 100644 index 00000000..59c3d403 --- /dev/null +++ b/Test/test2/Quantifiers.bpl.expect @@ -0,0 +1,20 @@ +Quantifiers.bpl(22,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(21,3): start +Quantifiers.bpl(45,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(44,3): start +Quantifiers.bpl(67,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(66,3): start +Quantifiers.bpl(75,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(73,3): start +Quantifiers.bpl(127,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(126,3): start +Quantifiers.bpl(152,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(151,3): start + +Boogie program verifier finished with 8 verified, 6 errors diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl index ed40787e..16d5bc82 100644 --- a/Test/test2/SelectiveChecking.bpl +++ b/Test/test2/SelectiveChecking.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure {:selective_checking} foo() { var x, y, z : int; diff --git a/Test/test2/SelectiveChecking.bpl.expect b/Test/test2/SelectiveChecking.bpl.expect new file mode 100644 index 00000000..8b5d33b0 --- /dev/null +++ b/Test/test2/SelectiveChecking.bpl.expect @@ -0,0 +1,16 @@ +SelectiveChecking.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + SelectiveChecking.bpl(17,3): anon0 +SelectiveChecking.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + SelectiveChecking.bpl(26,3): anon0 + SelectiveChecking.bpl(29,5): anon3_Then + SelectiveChecking.bpl(32,3): anon2 +SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold. +Execution trace: + SelectiveChecking.bpl(39,3): anon0 +SelectiveChecking.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + SelectiveChecking.bpl(39,3): anon0 + +Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl index d5ce8cf4..7a4ad46d 100644 --- a/Test/test2/Structured.bpl +++ b/Test/test2/Structured.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t const K: int; diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect new file mode 100644 index 00000000..cd8a1567 --- /dev/null +++ b/Test/test2/Structured.bpl.expect @@ -0,0 +1,20 @@ +Structured.bpl(254,14): Error BP5003: A postcondition might not hold on this return path. +Structured.bpl(245,3): Related location: This is the postcondition that might not hold. +Execution trace: + Structured.bpl(246,5): anon0 + Structured.bpl(248,5): anon6_LoopBody + Structured.bpl(249,7): anon7_LoopBody + Structured.bpl(250,11): anon8_Then + Structured.bpl(254,14): anon9_Then +Structured.bpl(305,3): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(301,5): anon0 + Structured.bpl(302,3): anon3_Else + Structured.bpl(305,3): anon2 +Structured.bpl(313,7): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(310,3): anon0 + Structured.bpl(310,3): anon1_Then + Structured.bpl(311,5): A + +Boogie program verifier finished with 16 verified, 3 errors diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index c874a1c1..51b6655f 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -timeLimit:4 %s > %t +// RUN: %diff %s.expect %t procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1); requires 0 < len; diff --git a/Test/test2/Timeouts0.bpl.expect b/Test/test2/Timeouts0.bpl.expect new file mode 100644 index 00000000..6c95b9bd --- /dev/null +++ b/Test/test2/Timeouts0.bpl.expect @@ -0,0 +1,47 @@ +Timeouts0.bpl(21,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(6,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(10,7): anon0 + Timeouts0.bpl(12,5): anon4_LoopHead + Timeouts0.bpl(12,5): anon4_LoopDone + Timeouts0.bpl(21,5): anon5_LoopHead + Timeouts0.bpl(21,5): anon5_LoopDone +Timeouts0.bpl(23,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(10,7): anon0 + Timeouts0.bpl(12,5): anon4_LoopHead + Timeouts0.bpl(12,5): anon4_LoopDone + Timeouts0.bpl(21,5): anon5_LoopHead + Timeouts0.bpl(25,11): anon5_LoopBody +Timeouts0.bpl(50,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(33,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(39,7): anon0 + Timeouts0.bpl(41,5): anon4_LoopHead + Timeouts0.bpl(41,5): anon4_LoopDone + Timeouts0.bpl(50,5): anon5_LoopHead + Timeouts0.bpl(50,5): anon5_LoopDone +Timeouts0.bpl(52,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(39,7): anon0 + Timeouts0.bpl(41,5): anon4_LoopHead + Timeouts0.bpl(41,5): anon4_LoopDone + Timeouts0.bpl(50,5): anon5_LoopHead + Timeouts0.bpl(54,11): anon5_LoopBody +Timeouts0.bpl(79,5): Error BP5003: A postcondition might not hold on this return path. +Timeouts0.bpl(62,3): Related location: This is the postcondition that might not hold. +Execution trace: + Timeouts0.bpl(68,7): anon0 + Timeouts0.bpl(70,5): anon4_LoopHead + Timeouts0.bpl(70,5): anon4_LoopDone + Timeouts0.bpl(79,5): anon5_LoopHead + Timeouts0.bpl(79,5): anon5_LoopDone +Timeouts0.bpl(81,7): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + Timeouts0.bpl(68,7): anon0 + Timeouts0.bpl(70,5): anon4_LoopHead + Timeouts0.bpl(70,5): anon4_LoopDone + Timeouts0.bpl(79,5): anon5_LoopHead + Timeouts0.bpl(83,11): anon5_LoopBody + +Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test2/TypeEncodingM.bpl b/Test/test2/TypeEncodingM.bpl index 01c95f7a..8a1bc803 100644 --- a/Test/test2/TypeEncodingM.bpl +++ b/Test/test2/TypeEncodingM.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m %s > %t +// RUN: %diff %s.expect %t type TT; procedure A() diff --git a/Test/test2/TypeEncodingM.bpl.expect b/Test/test2/TypeEncodingM.bpl.expect new file mode 100644 index 00000000..ea29f1d0 --- /dev/null +++ b/Test/test2/TypeEncodingM.bpl.expect @@ -0,0 +1,5 @@ +TypeEncodingM.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + TypeEncodingM.bpl(13,9): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl index 8f950073..d89c4715 100644 --- a/Test/test2/UpdateExpr.bpl +++ b/Test/test2/UpdateExpr.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t const a: [int]bool; diff --git a/Test/test2/UpdateExpr.bpl.expect b/Test/test2/UpdateExpr.bpl.expect new file mode 100644 index 00000000..30dc8529 --- /dev/null +++ b/Test/test2/UpdateExpr.bpl.expect @@ -0,0 +1,17 @@ +UpdateExpr.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(16,3): anon0 +UpdateExpr.bpl(21,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(21,3): anon0 +UpdateExpr.bpl(34,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(34,3): anon0 +UpdateExpr.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(40,3): anon0 +UpdateExpr.bpl(54,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(53,5): anon0 + +Boogie program verifier finished with 5 verified, 5 errors diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl index 96ffcf04..031398ed 100644 --- a/Test/test2/Where.bpl +++ b/Test/test2/Where.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t procedure P0() { var x: int where 0 <= x; diff --git a/Test/test2/Where.bpl.expect b/Test/test2/Where.bpl.expect new file mode 100644 index 00000000..a0399042 --- /dev/null +++ b/Test/test2/Where.bpl.expect @@ -0,0 +1,37 @@ +Where.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(8,3): anon0 +Where.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(18,5): anon0 +Where.bpl(34,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(32,3): anon0 +Where.bpl(46,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(42,5): anon0 +Where.bpl(59,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(54,3): anon0 +Where.bpl(113,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(104,5): anon0 + Where.bpl(106,3): anon3_LoopHead + Where.bpl(106,3): anon3_LoopDone +Where.bpl(130,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(123,5): anon0 + Where.bpl(124,3): anon3_LoopHead + Where.bpl(124,3): anon3_LoopDone +Where.bpl(147,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(140,5): anon0 + Where.bpl(141,3): anon3_LoopHead + Where.bpl(141,3): anon3_LoopDone +Where.bpl(164,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(157,5): anon0 + Where.bpl(158,3): anon3_LoopHead + Where.bpl(158,3): anon3_LoopDone + +Boogie program verifier finished with 2 verified, 9 errors diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl index df942317..1d902a74 100644 --- a/Test/test2/sk_hack.bpl +++ b/Test/test2/sk_hack.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t function in_set(int) returns(bool); function next(int) returns(int); function f(int) returns(bool); diff --git a/Test/test2/sk_hack.bpl.expect b/Test/test2/sk_hack.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test2/sk_hack.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index 6aee18ea..e451cc3e 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t type elements; diff --git a/Test/test2/strings-no-where.bpl.expect b/Test/test2/strings-no-where.bpl.expect new file mode 100644 index 00000000..df9c7d8b --- /dev/null +++ b/Test/test2/strings-no-where.bpl.expect @@ -0,0 +1,19 @@ +strings-no-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-no-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-no-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-no-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-no-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-no-where.bpl diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index f196899f..86804051 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t +// RUN: %diff %s.expect %t type elements; diff --git a/Test/test2/strings-where.bpl.expect b/Test/test2/strings-where.bpl.expect new file mode 100644 index 00000000..aa7fe2bb --- /dev/null +++ b/Test/test2/strings-where.bpl.expect @@ -0,0 +1,19 @@ +strings-where.bpl(203,103): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(205,105): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(211,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-where.bpl(213,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(213,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-where.bpl(213,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(215,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(237,98): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(251,118): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(701,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-where.bpl(730,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(739,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(753,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(762,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(928,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(951,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(977,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-where.bpl(992,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-where.bpl -- cgit v1.2.3