summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/inline/Answer121
-rw-r--r--Test/inline/expansion4.bpl31
-rw-r--r--Test/inline/runtest.bat3
3 files changed, 59 insertions, 96 deletions
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
<console>(68,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(57,0): inline$check$0$anon4_Else
- <console>(62,0): inline$check$0$anon3
- <console>(65,0): inline$check$0$Return
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(57,0): inline$check$0$anon4_Else
+ <console>(62,0): inline$check$0$anon3
+ <console>(65,0): inline$check$0$Return
<console>(100,4): Error BP5001: This assertion might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(52,0): inline$check$0$anon4_Then
- <console>(65,0): inline$check$0$Return
- <console>(73,0): inline$find$0$anon5_Then
- <console>(87,0): inline$find$0$anon3
- <console>(90,0): inline$find$0$Return
- <console>(95,0): anon0$1
- <console>(98,0): anon3_Then
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(52,0): inline$check$0$anon4_Then
+ <console>(65,0): inline$check$0$Return
+ <console>(73,0): inline$find$0$anon5_Then
+ <console>(87,0): inline$find$0$anon3
+ <console>(90,0): inline$find$0$Return
+ <console>(95,0): anon0$1
+ <console>(98,0): anon3_Then
<console>(50,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(10,0): anon0
- <console>(20,0): anon4_LoopBody
- <console>(24,0): inline$check$0$Entry
- <console>(39,0): inline$check$0$anon4_Else
- <console>(44,0): inline$check$0$anon3
- <console>(47,0): inline$check$0$Return
+ <console>(10,0): anon0
+ <console>(20,0): anon4_LoopBody
+ <console>(24,0): inline$check$0$Entry
+ <console>(39,0): inline$check$0$anon4_Else
+ <console>(44,0): inline$check$0$anon3
+ <console>(47,0): inline$check$0$Return
<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(85,0): anon0
- <console>(93,0): anon4_Else
- <console>(98,0): anon3
+ <console>(85,0): anon0
+ <console>(93,0): anon4_Else
+ <console>(98,0): anon3
Boogie program verifier finished with 0 verified, 4 errors
-------------------- test6.bpl --------------------
@@ -1442,10 +1442,10 @@ Boogie program verifier finished with 5 verified, 0 errors
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- test5.bpl(34,10): anon0
- test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(34,10): anon0$2
+ test5.bpl(34,10): anon0
+ test5.bpl(28,10): inline$P$0$anon0
+ test5.bpl(28,10): inline$P$1$anon0
+ test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
-------------------- expansion.bpl --------------------
@@ -1465,37 +1465,37 @@ expansion.bpl(33,22): Error: expansion: an identifier was used more than once
*** more than one possible expansion for x1
expansion3.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- expansion3.bpl(18,3): anon0
+ expansion3.bpl(18,3): anon0
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl with empty blocks --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(68,23): inline$Initialize$0$Entry
- Elevator.bpl(71,13): inline$Initialize$0$anon0
- Elevator.bpl(68,23): inline$Initialize$0$Return
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(19,5): anon11_Else
- Elevator.bpl(19,5): anon12_Else
- Elevator.bpl(24,7): anon13_Then
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Entry
+ Elevator.bpl(71,13): inline$Initialize$0$anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Return
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(19,5): anon11_Else
+ Elevator.bpl(19,5): anon12_Else
+ Elevator.bpl(24,7): anon13_Then
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- expansion2.bpl --------------------
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 04:31:00 +0000