summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/aitest0/runtest.bat2
-rw-r--r--Test/aitest1/runtest.bat2
-rw-r--r--Test/aitest9/answer3
-rw-r--r--Test/dafny0/Answer3
-rw-r--r--Test/inline/Answer16
-rw-r--r--Test/inline/runtest.bat7
-rw-r--r--Test/livevars/Answer15
-rw-r--r--Test/smoke/Answer4
-rw-r--r--Test/test2/Answer20
-rw-r--r--Test/test2/ContractEvaluationOrder.bpl34
-rw-r--r--Test/test2/Structured.bpl2
-rw-r--r--Test/test2/runtest.bat2
12 files changed, 90 insertions, 20 deletions
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index 15f36ab0..a4c12d8d 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -3,4 +3,4 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-%BGEXE% %* -infer:c -printInstrumented -noVerify constants.bpl
+%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl
diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat
index f2a4d3e5..3b2c382c 100644
--- a/Test/aitest1/runtest.bat
+++ b/Test/aitest1/runtest.bat
@@ -7,7 +7,7 @@ for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl
Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl
Linear7.bpl Linear8.bpl Linear9.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% %* -infer:p -printInstrumented -noVerify %%f
+ %BGEXE% %* -infer:p -instrumentInfer:e -printInstrumented -noVerify %%f
)
for %%f in (Bound.bpl) do (
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
index d6bba688..27e18ca4 100644
--- a/Test/aitest9/answer
+++ b/Test/aitest9/answer
@@ -13,11 +13,8 @@ TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
TestIntervals.bpl(5,5): anon0
TestIntervals.bpl(6,3): anon9_LoopHead
- TestIntervals.bpl(6,3): anon9_LoopDone
TestIntervals.bpl(12,14): anon10_Then
- TestIntervals.bpl(13,3): anon4
TestIntervals.bpl(13,14): anon11_Then
- TestIntervals.bpl(14,3): anon6
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 107cab0b..540bcb4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -87,17 +87,14 @@ Execution trace:
(0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
- (0,0): anon0
(0,0): anon10_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
- (0,0): anon0
(0,0): anon10_Else
(0,0): anon3
(0,0): anon11_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
- (0,0): anon0
(0,0): anon10_Then
(0,0): anon3
(0,0): anon11_Then
diff --git a/Test/inline/Answer b/Test/inline/Answer
index 934b45ba..12cb5960 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1443,13 +1443,8 @@ Boogie program verifier finished with 5 verified, 0 errors
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
test5.bpl(34,10): anon0
- test5.bpl(25,23): inline$P$0$Entry
test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(25,23): inline$P$0$Return
- test5.bpl(34,10): anon0$1
- test5.bpl(25,23): inline$P$1$Entry
test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(25,23): inline$P$1$Return
test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
@@ -1477,6 +1472,17 @@ Boogie program verifier finished with 1 verified, 1 error
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
+
+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
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 335c857d..179509f8 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -18,6 +18,13 @@ for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
%BGEXE% %* %%f
)
+REM Peephole optimizations are so good that Elevator seems worthwhile
+REM to include twice among these inline tests
+for %%f in (Elevator.bpl) do (
+ echo -------------------- %%f with empty blocks --------------------
+ %BGEXE% /removeEmptyBlocks:0 %* %%f
+)
+
echo -------------------- expansion2.bpl --------------------
%BGEXE% %* /proverLog:expansion2.sx expansion2.bpl
%SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx
diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index aaaee494..1a0327f6 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -51,6 +51,7 @@ Execution trace:
bla1.bpl(1654,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1
+ bla1.bpl(1676,3): inline$storm_IoCompleteRequest$0$label_1#1
bla1.bpl(1734,3): anon14_Then#1
bla1.bpl(1739,3): anon7#1
bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1
@@ -144,6 +145,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(1872,3): inline$storm_KeAcquireSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(1883,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1888,3): inline$storm_KeAcquireSpinLock$0$anon9#2
+ daytona_bug2_ioctl_example_2.bpl(1892,3): inline$storm_KeAcquireSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(1909,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
daytona_bug2_ioctl_example_2.bpl(1920,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
@@ -155,6 +157,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2039,3): inline$storm_IoSetCancelRoutine$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(2050,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2055,3): inline$storm_IoSetCancelRoutine$0$anon10#2
+ daytona_bug2_ioctl_example_2.bpl(2062,3): inline$storm_IoSetCancelRoutine$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2
daytona_bug2_ioctl_example_2.bpl(2075,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
daytona_bug2_ioctl_example_2.bpl(2200,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
@@ -170,6 +173,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2337,3): inline$storm_IoSetCancelRoutine$1$anon8#2
daytona_bug2_ioctl_example_2.bpl(2348,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2353,3): inline$storm_IoSetCancelRoutine$1$anon10#2
+ daytona_bug2_ioctl_example_2.bpl(2361,3): inline$storm_IoSetCancelRoutine$1$label_1#2
daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2
daytona_bug2_ioctl_example_2.bpl(2375,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
daytona_bug2_ioctl_example_2.bpl(2385,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
@@ -185,6 +189,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2599,3): inline$storm_KeReleaseSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(2610,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(2615,3): inline$storm_KeReleaseSpinLock$0$anon7#2
+ daytona_bug2_ioctl_example_2.bpl(2619,3): inline$storm_KeReleaseSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
daytona_bug2_ioctl_example_2.bpl(2858,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51#2
@@ -194,10 +199,12 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2951,3): inline$storm_IoCompleteRequest$2$anon6_Else#2
daytona_bug2_ioctl_example_2.bpl(2959,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
daytona_bug2_ioctl_example_2.bpl(2969,3): inline$storm_IoCompleteRequest$2$anon2#2
+ daytona_bug2_ioctl_example_2.bpl(2973,3): inline$storm_IoCompleteRequest$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#2
daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
daytona_bug2_ioctl_example_2.bpl(3000,3): inline$I8xCompleteSysButtonIrp$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
+ daytona_bug2_ioctl_example_2.bpl(3013,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2
daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3169,3): inline$I8xKeyboardGetSysButtonEvent$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2
@@ -222,6 +229,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(3931,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3942,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(3947,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
+ daytona_bug2_ioctl_example_2.bpl(3951,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3964,3): inline$storm_IoCancelIrp$0$anon30_Else#2
daytona_bug2_ioctl_example_2.bpl(3982,3): inline$storm_IoCancelIrp$0$label_16_true#2
@@ -293,6 +301,7 @@ Execution trace:
stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1
stack_overflow.bpl(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
+ stack_overflow.bpl(78233,3): inline$storm_IoSetCompletionRoutine$0$label_1#1
stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1
stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
@@ -330,11 +339,13 @@ Execution trace:
stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
stack_overflow.bpl(87671,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
stack_overflow.bpl(87685,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
+ stack_overflow.bpl(87692,3): inline$BDLDevicePowerIoCompletion$3$label_83#1
stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
stack_overflow.bpl(87702,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1
stack_overflow.bpl(87713,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1
stack_overflow.bpl(87738,3): inline$storm_IoCompleteRequest$7$label_6_false#1
stack_overflow.bpl(87777,3): inline$storm_IoCompleteRequest$7$label_7#1
+ stack_overflow.bpl(87782,3): inline$storm_IoCompleteRequest$7$label_1#1
stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#1
stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
@@ -344,13 +355,16 @@ Execution trace:
stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
stack_overflow.bpl(87953,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
stack_overflow.bpl(87967,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
+ stack_overflow.bpl(87974,3): inline$BDLDevicePowerIoCompletion$3$label_122#1
stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1
stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1
stack_overflow.bpl(88146,3): inline$CallCompletionRoutine$3$label_20_icall_return#1
stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1
+ stack_overflow.bpl(88169,3): inline$CallCompletionRoutine$3$label_1#1
stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1
stack_overflow.bpl(88190,3): inline$storm_IoCallDriver$1$anon15_Else#1
stack_overflow.bpl(88218,3): inline$storm_IoCallDriver$1$label_36#1
+ stack_overflow.bpl(88222,3): inline$storm_IoCallDriver$1$label_1#1
stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#1
stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1
stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1
@@ -373,6 +387,7 @@ Execution trace:
stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1
stack_overflow.bpl(89292,3): inline$BDLPnPStart$0$anon46_Else#1
stack_overflow.bpl(89306,3): inline$BDLPnPStart$0$label_101_true#1
+ stack_overflow.bpl(89313,3): inline$BDLPnPStart$0$label_102#1
stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#1
stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1
stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1
diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index 5fb6fe62..de255422 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -6,15 +6,11 @@ implementation b(x: int)
anon0:
- assume true;
- assume true;
goto anon3_Then;
anon3_Then:
- assume true;
assume x < 0;
y := 1;
- assume 1 <= y && y <= 1;
assert false;
return;
}
diff --git a/Test/test2/Answer b/Test/test2/Answer
index ef808373..8abc36c9 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -34,6 +34,7 @@ Execution trace:
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
@@ -213,14 +214,16 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar
Structured.bpl(252,14): Error BP5003: A postcondition might not hold 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(244,5): anon0
Structured.bpl(246,5): anon6_LoopBody
Structured.bpl(247,7): anon7_LoopBody
+ Structured.bpl(248,11): anon8_Then
Structured.bpl(252,5): anon4
Structured.bpl(252,14): anon9_Then
Structured.bpl(303,3): Error BP5001: This assertion might not hold.
Execution trace:
Structured.bpl(299,5): anon0
+ Structured.bpl(300,3): anon3_Else
Structured.bpl(303,3): anon2
Structured.bpl(311,7): Error BP5001: This assertion might not hold.
Execution trace:
@@ -378,3 +381,18 @@ Execution trace:
CallForall.bpl(124,3): anon0
Boogie program verifier finished with 10 verified, 8 errors
+
+-------------------- ContractEvaluationOrder.bpl --------------------
+ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.
+ContractEvaluationOrder.bpl(3,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.
+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.
+Execution trace:
+ ContractEvaluationOrder.bpl(23,5): anon0
+
+Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
new file mode 100644
index 00000000..3eab4bda
--- /dev/null
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -0,0 +1,34 @@
+procedure P() returns (x, y: int)
+ ensures x == y; // ensured by the body
+ ensures x == 0; // error: not ensured by the body
+ ensures y == 0; // follows from the previous two ensures clauses (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+{
+ x := y;
+}
+
+procedure Q() returns (x, y: int)
+{
+ x := y;
+
+ assert x == y; // ensured by the body
+ assert x == 0; // error: not ensured by the body
+ assert y == 0; // follows from the previous two asserts (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+}
+
+procedure R()
+{
+ var a, b: int;
+ a := b;
+ call S(a, b);
+}
+
+procedure S(x, y: int)
+ // In the call from R:
+ requires x == y; // ensured by the body of R
+ requires x == 0; // error: not ensured by the body of R
+ requires y == 0; // follows from the previous two requires clauses (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+{
+}
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index ce97b145..69ea2576 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -241,7 +241,7 @@ procedure RunOffEnd2() returns (x: int)
procedure RunOffEnd3() returns (x: int)
ensures x == 9;
-{
+{ x := 9;
while (true) {
while (true) {
if (*) {
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f472741c..dbe5b726 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
echo -------------------- sk_hack.bpl --------------------
%BGEXE% %* /noinfer /bv:z sk_hack.bpl
-for %%f in (CallForall.bpl) do (
+for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* %%f
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 20:01:46 +0000