From faf1c46b1e67ab4c3d8a1c82974b0499015a83d3 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 7 Aug 2009 17:21:13 +0000 Subject: Removed Output files. These are created on a local machine when the tests are run. --- Test/test2/Output | 359 ------------------------------------------------------ 1 file changed, 359 deletions(-) delete mode 100644 Test/test2/Output (limited to 'Test/test2') diff --git a/Test/test2/Output b/Test/test2/Output deleted file mode 100644 index 7876d732..00000000 --- a/Test/test2/Output +++ /dev/null @@ -1,359 +0,0 @@ - --------------------- FormulaTerm.bpl -------------------- -FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement. -FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold. -Execution trace: - 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(47,5): Error BP5001: This assertion might not hold. -Execution trace: - FormulaTerm2.bpl(45,3): start - -Boogie program verifier finished with 2 verified, 2 errors - --------------------- Passification.bpl -------------------- -Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement. -Passification.bpl(36,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. -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. -Execution trace: - 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 - -Boogie program verifier finished with 7 verified, 4 errors - --------------------- B.bpl -------------------- - -Boogie program verifier finished with 4 verified, 0 errors - --------------------- Ensures.bpl -------------------- -Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. -Execution trace: - Ensures.bpl(28,3): start -Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. -Execution trace: - Ensures.bpl(34,3): start -Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. -Execution trace: - Ensures.bpl(39,3): start -Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. -Execution trace: - Ensures.bpl(45,3): start -Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement. -Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. -Execution trace: - Ensures.bpl(70,3): start - -Boogie program verifier finished with 5 verified, 5 errors - --------------------- Old.bpl -------------------- -Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement. -Old.bpl(26,3): Related location: This is the postcondition that might not hold. -Execution trace: - Old.bpl(28,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 -2 name resolution errors detected in OldIllegal.bpl - --------------------- Arrays.bpl -------------------- -Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement. -Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. -Execution trace: - Arrays.bpl(42,3): start -Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement. -Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. -Execution trace: - 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 - -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(43,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. -Execution trace: - 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(125,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. -Execution trace: - 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(46,5): Error BP5001: This assertion might not hold. -Execution trace: - Call.bpl(45,3): start -Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement. -Call.bpl(20,3): Related location: This is the postcondition that might not hold. -Execution trace: - 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(47,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. -Execution trace: - 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 - -Boogie program verifier finished with 0 verified, 1 error - --------------------- False.bpl -------------------- - -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 - -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 == -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 == -18 type checking errors detected in strings-where.bpl - --------------------- Structured.bpl -------------------- -Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement. -Structured.bpl(243,3): Related location: This is the postcondition that might not hold. -Execution trace: - Structured.bpl(245,3): anon0 - Structured.bpl(245,3): anon6_LoopHead - Structured.bpl(246,5): anon6_LoopBody - Structured.bpl(247,7): anon7_LoopBody - 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(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 - -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(22,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. -Execution trace: - 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(57,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. -Execution trace: - Where.bpl(102,5): anon0 - Where.bpl(104,3): anon3_LoopHead - Where.bpl(110,3): anon2 -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(125,3): anon2 -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(142,3): anon2 -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(159,3): anon2 - -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(19,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. -Execution trace: - 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(52,3): Error BP5001: This assertion might not hold. -Execution trace: - 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(22,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. -Execution trace: - 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(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. -Execution trace: - 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(15,3): Error BP5001: This assertion might not hold. -Execution trace: - Implies.bpl(11,3): anon0 - -Boogie program verifier finished with 0 verified, 2 errors --------------------- sk_hack.bpl -------------------- - -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(29,3): Error BP5001: This assertion might not hold. -Execution trace: - 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(47,3): Error BP5001: This assertion might not hold. -Execution trace: - 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(111,3): Error BP5001: This assertion might not hold. -Execution trace: - 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(125,3): Error BP5001: This assertion might not hold. -Execution trace: - CallForall.bpl(124,3): anon0 - -Boogie program verifier finished with 10 verified, 8 errors -- cgit v1.2.3