From 2e4c60cba8c332250ee1a88fa62744eec0034763 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Fri, 18 Feb 2011 22:04:41 +0000 Subject: Remove a testcase for bvInt (feature to be killed soon) --- Test/inline/Answer | 121 ++++++++++++++++++++++----------------------- Test/inline/expansion4.bpl | 31 ------------ Test/inline/runtest.bat | 3 -- 3 files changed, 59 insertions(+), 96 deletions(-) delete mode 100644 Test/inline/expansion4.bpl (limited to 'Test/inline') diff --git a/Test/inline/Answer b/Test/inline/Answer index 0820093a..72ba1170 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1,8 +1,8 @@ -------------------- test0.bpl -------------------- test0.bpl(30,5): Error BP5001: This assertion might not hold. Execution trace: - test0.bpl(26,3): anon0 - test0.bpl(30,5): anon3_Then + test0.bpl(26,3): anon0 + test0.bpl(30,5): anon3_Then Boogie program verifier finished with 1 verified, 1 error -------------------- test1.bpl -------------------- @@ -822,41 +822,41 @@ implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bo (68,4): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: - (19,0): anon0 - (28,0): inline$find$0$anon0 - (38,0): inline$find$0$anon4_LoopBody - (42,0): inline$check$0$Entry - (57,0): inline$check$0$anon4_Else - (62,0): inline$check$0$anon3 - (65,0): inline$check$0$Return + (19,0): anon0 + (28,0): inline$find$0$anon0 + (38,0): inline$find$0$anon4_LoopBody + (42,0): inline$check$0$Entry + (57,0): inline$check$0$anon4_Else + (62,0): inline$check$0$anon3 + (65,0): inline$check$0$Return (100,4): Error BP5001: This assertion might not hold. Execution trace: - (19,0): anon0 - (28,0): inline$find$0$anon0 - (38,0): inline$find$0$anon4_LoopBody - (42,0): inline$check$0$Entry - (52,0): inline$check$0$anon4_Then - (65,0): inline$check$0$Return - (73,0): inline$find$0$anon5_Then - (87,0): inline$find$0$anon3 - (90,0): inline$find$0$Return - (95,0): anon0$1 - (98,0): anon3_Then + (19,0): anon0 + (28,0): inline$find$0$anon0 + (38,0): inline$find$0$anon4_LoopBody + (42,0): inline$check$0$Entry + (52,0): inline$check$0$anon4_Then + (65,0): inline$check$0$Return + (73,0): inline$find$0$anon5_Then + (87,0): inline$find$0$anon3 + (90,0): inline$find$0$Return + (95,0): anon0$1 + (98,0): anon3_Then (50,4): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: - (10,0): anon0 - (20,0): anon4_LoopBody - (24,0): inline$check$0$Entry - (39,0): inline$check$0$anon4_Else - (44,0): inline$check$0$anon3 - (47,0): inline$check$0$Return + (10,0): anon0 + (20,0): anon4_LoopBody + (24,0): inline$check$0$Entry + (39,0): inline$check$0$anon4_Else + (44,0): inline$check$0$anon3 + (47,0): inline$check$0$Return (99,0): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: - (85,0): anon0 - (93,0): anon4_Else - (98,0): anon3 + (85,0): anon0 + (93,0): anon4_Else + (98,0): anon3 Boogie program verifier finished with 0 verified, 4 errors -------------------- test6.bpl -------------------- @@ -1442,10 +1442,10 @@ Boogie program verifier finished with 5 verified, 0 errors -------------------- test5.bpl -------------------- test5.bpl(37,3): Error BP5001: This assertion might not hold. Execution trace: - test5.bpl(34,10): anon0 - test5.bpl(28,10): inline$P$0$anon0 - test5.bpl(28,10): inline$P$1$anon0 - test5.bpl(34,10): anon0$2 + test5.bpl(34,10): anon0 + test5.bpl(28,10): inline$P$0$anon0 + test5.bpl(28,10): inline$P$1$anon0 + test5.bpl(34,10): anon0$2 Boogie program verifier finished with 4 verified, 1 error -------------------- expansion.bpl -------------------- @@ -1465,37 +1465,37 @@ expansion.bpl(33,22): Error: expansion: an identifier was used more than once *** more than one possible expansion for x1 expansion3.bpl(18,3): Error BP5001: This assertion might not hold. Execution trace: - expansion3.bpl(18,3): anon0 + expansion3.bpl(18,3): anon0 Boogie program verifier finished with 1 verified, 1 error -------------------- Elevator.bpl -------------------- Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop. Execution trace: - Elevator.bpl(15,3): anon0 - Elevator.bpl(15,3): anon0$1 - Elevator.bpl(16,3): anon10_LoopHead - Elevator.bpl(19,5): anon10_LoopBody - Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0 - Elevator.bpl(24,7): anon13_Then$1 + Elevator.bpl(15,3): anon0 + Elevator.bpl(15,3): anon0$1 + Elevator.bpl(16,3): anon10_LoopHead + Elevator.bpl(19,5): anon10_LoopBody + Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0 + Elevator.bpl(24,7): anon13_Then$1 Boogie program verifier finished with 1 verified, 1 error -------------------- Elevator.bpl with empty blocks -------------------- Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop. Execution trace: - Elevator.bpl(15,3): anon0 - Elevator.bpl(68,23): inline$Initialize$0$Entry - Elevator.bpl(71,13): inline$Initialize$0$anon0 - Elevator.bpl(68,23): inline$Initialize$0$Return - Elevator.bpl(15,3): anon0$1 - Elevator.bpl(16,3): anon10_LoopHead - Elevator.bpl(19,5): anon10_LoopBody - Elevator.bpl(19,5): anon11_Else - Elevator.bpl(19,5): anon12_Else - Elevator.bpl(24,7): anon13_Then - Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry - Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0 - Elevator.bpl(94,23): inline$MoveDown_Error$0$Return - Elevator.bpl(24,7): anon13_Then$1 + Elevator.bpl(15,3): anon0 + Elevator.bpl(68,23): inline$Initialize$0$Entry + Elevator.bpl(71,13): inline$Initialize$0$anon0 + Elevator.bpl(68,23): inline$Initialize$0$Return + Elevator.bpl(15,3): anon0$1 + Elevator.bpl(16,3): anon10_LoopHead + Elevator.bpl(19,5): anon10_LoopBody + Elevator.bpl(19,5): anon11_Else + Elevator.bpl(19,5): anon12_Else + Elevator.bpl(24,7): anon13_Then + Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry + Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0 + Elevator.bpl(94,23): inline$MoveDown_Error$0$Return + Elevator.bpl(24,7): anon13_Then$1 Boogie program verifier finished with 1 verified, 1 error -------------------- expansion2.bpl -------------------- @@ -1505,9 +1505,6 @@ Boogie program verifier finished with 1 verified, 0 errors ---------- EXPANSION2.SX: 0 ---------- EXPANSION2.SX: 0 --------------------- expansion4.bpl -------------------- - -Boogie program verifier finished with 3 verified, 0 errors -------------------- fundef.bpl -------------------- function {:inline true} foo(x: int) : bool @@ -1528,7 +1525,7 @@ axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); Boogie program verifier finished with 0 verified, 0 errors fundef2.bpl(6,3): Error BP5001: This assertion might not hold. Execution trace: - fundef2.bpl(5,3): anon0 + fundef2.bpl(5,3): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- polyInline.bpl -------------------- @@ -1537,10 +1534,10 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int polyInline.bpl(23,3): Error BP5001: This assertion might not hold. Execution trace: - polyInline.bpl(20,3): anon0 + polyInline.bpl(20,3): anon0 polyInline.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - polyInline.bpl(27,3): anon0 + polyInline.bpl(27,3): anon0 Boogie program verifier finished with 0 verified, 2 errors polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int @@ -1548,9 +1545,9 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int polyInline.bpl(23,3): Error BP5001: This assertion might not hold. Execution trace: - polyInline.bpl(20,3): anon0 + polyInline.bpl(20,3): anon0 polyInline.bpl(39,3): Error BP5001: This assertion might not hold. Execution trace: - polyInline.bpl(27,3): anon0 + polyInline.bpl(27,3): anon0 Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl deleted file mode 100644 index 593fa9fb..00000000 --- a/Test/inline/expansion4.bpl +++ /dev/null @@ -1,31 +0,0 @@ -function f(x:int) returns(bool); -axiom {:ignore "bvInt"} {:inline true} (forall x:int :: f(x) <==> true); -axiom {:ignore "bvDefSem"} {:inline true} (forall x:int :: f(x) <==> false); - -procedure {:forceBvZ3Native true} foo() -{ - assert f(3); -} - -procedure {:forceBvInt true} foo2() -{ - assert !f(3); -} - -axiom (forall x: bv64, y: bv64 :: { $sub.unchk.u8(x, y) } $check.sub.u8(x, y) ==> $sub.u8(x, y) == $sub.unchk.u8(x, y)); -axiom {:inline true} {:ignore "bvDefSem"} (forall x: bv64, y: bv64 :: { $check.sub.u8(x, y) } -$check.sub.u8(x, y) <==> $_inrange.u8($sub.i8(x, y))); - -function $check.sub.u8(x: bv64, y: bv64) returns (bool); -function $_inrange.u8(bv64) returns (bool); -function {:bvbuiltin "bvsub"} $sub.unchk.u8(x: bv64, y: bv64) returns (bv64); -function {:bvbuiltin "bvsub"} {:bvint "-"} $sub.i8(x: bv64, y: bv64) returns (bv64); -function {:bvbuiltin "bvsub"} {:bvint "-"} $sub.u8(x: bv64, y: bv64) returns (bv64); - - -procedure {:forceBvZ3Native true} baz() -{ - return; -} - - diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index 179509f8..f04b84da 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -30,9 +30,6 @@ echo -------------------- expansion2.bpl -------------------- %SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx %SystemRoot%\system32\find.exe /C "xxf1" expansion2.sx -echo -------------------- expansion4.bpl -------------------- -%BGEXE% %* /bv:i expansion4.bpl - echo -------------------- fundef.bpl -------------------- %BGEXE% %* /print:- /env:0 fundef.bpl %BGEXE% %* fundef2.bpl -- cgit v1.2.3