Implemented block coalescing invoked right after type checking.

Controlled by the option /coalesceBlocks (default is to perform the optimization).

1 files changed, 8 insertions, 170 deletions

diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index d958205f..aaaee494 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -4,16 +4,12 @@ Execution trace:
     bla1.bpl(789,3): anon10_Then#1

     bla1.bpl(794,3): anon2#1

     bla1.bpl(822,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1

-    bla1.bpl(830,3): inline$storm_IoAllocateIrp$0$label_13#1

     bla1.bpl(854,3): inline$storm_IoAllocateIrp$0$anon14_Then#1

     bla1.bpl(859,3): inline$storm_IoAllocateIrp$0$anon2#1

     bla1.bpl(879,3): inline$storm_IoAllocateIrp$0$anon16_Then#1

     bla1.bpl(884,3): inline$storm_IoAllocateIrp$0$anon5#1

     bla1.bpl(904,3): inline$storm_IoAllocateIrp$0$anon18_Then#1

     bla1.bpl(909,3): inline$storm_IoAllocateIrp$0$anon8#1

-    bla1.bpl(913,3): inline$storm_IoAllocateIrp$0$label_20#1

-    bla1.bpl(917,3): inline$storm_IoAllocateIrp$0$label_21#1

-    bla1.bpl(921,3): inline$storm_IoAllocateIrp$0$label_22#1

     bla1.bpl(945,3): inline$storm_IoAllocateIrp$0$anon20_Then#1

     bla1.bpl(950,3): inline$storm_IoAllocateIrp$0$anon11#1

     bla1.bpl(981,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1

@@ -21,12 +17,6 @@ Execution trace:
     bla1.bpl(1018,3): inline$storm_IoAllocateIrp$0$anon22_Then#1

     bla1.bpl(1023,3): inline$storm_IoAllocateIrp$0$anon13#1

     bla1.bpl(1035,3): inline$storm_IoAllocateIrp$0$label_36#1

-    bla1.bpl(1039,3): inline$storm_IoAllocateIrp$0$label_1#1

-    bla1.bpl(1042,3): inline$storm_IoAllocateIrp$0$Return#1

-    bla1.bpl(1046,3): label_6$1#1

-    bla1.bpl(1049,3): label_9#1

-    bla1.bpl(1053,3): label_10#1

-    bla1.bpl(1068,3): inline$IoSetNextIrpStackLocation$0$label_3#1

     bla1.bpl(1089,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1

     bla1.bpl(1094,3): inline$IoSetNextIrpStackLocation$0$anon2#1

     bla1.bpl(1112,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1

@@ -35,7 +25,6 @@ Execution trace:
     bla1.bpl(1162,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1

     bla1.bpl(1197,3): anon12_Then#1

     bla1.bpl(1202,3): anon5#1

-    bla1.bpl(1209,3): label_20#1

     bla1.bpl(1255,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1

     bla1.bpl(1259,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1

     bla1.bpl(1308,3): inline$I8xDeviceControl$0$anon3_Then#1

@@ -43,7 +32,6 @@ Execution trace:
     bla1.bpl(1348,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1

     bla1.bpl(1376,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1

     bla1.bpl(1408,3): inline$storm_IoSetCancelRoutine$0$label_8#1

-    bla1.bpl(1412,3): inline$storm_IoSetCancelRoutine$0$label_16#1

     bla1.bpl(1415,3): inline$storm_IoSetCancelRoutine$0$anon9_Else#1

     bla1.bpl(1423,3): inline$storm_IoSetCancelRoutine$0$anon10_Then#1

     bla1.bpl(1431,3): inline$storm_IoSetCancelRoutine$0$anon3#1

@@ -56,7 +44,6 @@ Execution trace:
     bla1.bpl(1532,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1

     bla1.bpl(1542,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1

     bla1.bpl(1566,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1

-    bla1.bpl(1570,3): inline$I8xKeyboardGetSysButtonEvent$0$label_27#1

     bla1.bpl(1579,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13#1

     bla1.bpl(1586,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1

     bla1.bpl(1619,3): inline$storm_IoCompleteRequest$0$label_6_false#1

@@ -65,7 +52,7 @@ Execution trace:
     bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1

     bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1

     bla1.bpl(1734,3): anon14_Then#1

-    bla1.bpl(1747,3): label_24#1

+    bla1.bpl(1739,3): anon7#1

     bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1

     bla1.bpl(1801,3): inline$storm_IoCancelIrp$0$anon2#1

     bla1.bpl(1812,3): inline$storm_IoCancelIrp$0$anon14_Else#1

@@ -76,9 +63,7 @@ Execution trace:
     bla1.bpl(1856,3): inline$storm_IoCancelIrp$0$anon8#1

     bla1.bpl(1867,3): inline$storm_IoCancelIrp$0$anon18_Then#1

     bla1.bpl(1872,3): inline$storm_IoCancelIrp$0$anon10#1

-    bla1.bpl(1876,3): inline$storm_IoCancelIrp$0$label_13#1

     bla1.bpl(1932,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1

-    bla1.bpl(1938,3): inline$storm_IoAcquireCancelSpinLock$0$label_15#1

     bla1.bpl(1947,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1

     bla1.bpl(1955,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_Then#1

     bla1.bpl(1965,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1

@@ -86,16 +71,10 @@ Execution trace:
     bla1.bpl(1981,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1

     bla1.bpl(2005,3): inline$storm_IoCancelIrp$0$label_16_true#1

     bla1.bpl(2023,3): inline$storm_IoCancelIrp$0$label_22_true#1

-    bla1.bpl(2027,3): inline$storm_IoCancelIrp$0$label_24#1

     bla1.bpl(2036,3): inline$storm_IoCancelIrp$0$label_25_false#1

     bla1.bpl(2054,3): inline$storm_IoCancelIrp$0$label_1#1

-    bla1.bpl(2057,3): inline$storm_IoCancelIrp$0$Return#1

-    bla1.bpl(2060,3): inline$cancel$0$label_3$1#1

-    bla1.bpl(2063,3): inline$cancel$0$label_1#1

-    bla1.bpl(2066,3): inline$cancel$0$Return#1

-    bla1.bpl(2069,3): label_24$1#1

     bla1.bpl(2076,3): anon15_Then#1

-    bla1.bpl(2086,3): label_1#1

+    bla1.bpl(2081,3): anon9#1

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -106,7 +85,6 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(846,3): anon22_Then#2

     daytona_bug2_ioctl_example_2.bpl(851,3): anon2#2

     daytona_bug2_ioctl_example_2.bpl(879,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2

-    daytona_bug2_ioctl_example_2.bpl(887,3): inline$storm_IoAllocateIrp$0$label_13#2

     daytona_bug2_ioctl_example_2.bpl(911,3): inline$storm_IoAllocateIrp$0$anon18_Then#2

     daytona_bug2_ioctl_example_2.bpl(916,3): inline$storm_IoAllocateIrp$0$anon2#2

     daytona_bug2_ioctl_example_2.bpl(936,3): inline$storm_IoAllocateIrp$0$anon20_Then#2

@@ -114,9 +92,6 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(961,3): inline$storm_IoAllocateIrp$0$anon22_Then#2

     daytona_bug2_ioctl_example_2.bpl(966,3): inline$storm_IoAllocateIrp$0$anon8#2

     daytona_bug2_ioctl_example_2.bpl(974,3): inline$storm_IoAllocateIrp$0$anon24_Else#2

-    daytona_bug2_ioctl_example_2.bpl(978,3): inline$storm_IoAllocateIrp$0$anon10#2

-    daytona_bug2_ioctl_example_2.bpl(982,3): inline$storm_IoAllocateIrp$0$label_21#2

-    daytona_bug2_ioctl_example_2.bpl(986,3): inline$storm_IoAllocateIrp$0$label_22#2

     daytona_bug2_ioctl_example_2.bpl(1010,3): inline$storm_IoAllocateIrp$0$anon25_Then#2

     daytona_bug2_ioctl_example_2.bpl(1015,3): inline$storm_IoAllocateIrp$0$anon13#2

     daytona_bug2_ioctl_example_2.bpl(1046,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2

@@ -125,11 +100,8 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1090,3): inline$storm_IoAllocateIrp$0$anon28_Then#2

     daytona_bug2_ioctl_example_2.bpl(1095,3): inline$storm_IoAllocateIrp$0$anon17#2

     daytona_bug2_ioctl_example_2.bpl(1115,3): inline$storm_IoAllocateIrp$0$label_36#2

-    daytona_bug2_ioctl_example_2.bpl(1119,3): inline$storm_IoAllocateIrp$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(1129,3): anon24_Else#2

     daytona_bug2_ioctl_example_2.bpl(1144,3): anon25_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1148,3): anon6#2

-    daytona_bug2_ioctl_example_2.bpl(1163,3): inline$IoSetNextIrpStackLocation$0$label_3#2

     daytona_bug2_ioctl_example_2.bpl(1184,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2

     daytona_bug2_ioctl_example_2.bpl(1189,3): inline$IoSetNextIrpStackLocation$0$anon2#2

     daytona_bug2_ioctl_example_2.bpl(1207,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2

@@ -142,15 +114,11 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1311,3): anon13#2

     daytona_bug2_ioctl_example_2.bpl(1343,3): inline$myInitDriver$0$anon5_Then#2

     daytona_bug2_ioctl_example_2.bpl(1348,3): inline$myInitDriver$0$anon2#2

-    daytona_bug2_ioctl_example_2.bpl(1353,3): inline$myInitDriver$0$label_5#2

-    daytona_bug2_ioctl_example_2.bpl(1359,3): inline$storm_KeInitializeSpinLock$0$Entry#2

     daytona_bug2_ioctl_example_2.bpl(1383,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2

     daytona_bug2_ioctl_example_2.bpl(1388,3): inline$storm_KeInitializeSpinLock$0$anon2#2

     daytona_bug2_ioctl_example_2.bpl(1401,3): inline$myInitDriver$0$anon7_Else#2

     daytona_bug2_ioctl_example_2.bpl(1416,3): inline$myInitDriver$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(1419,3): label_19$1#2

     daytona_bug2_ioctl_example_2.bpl(1422,3): anon30_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1432,3): label_23#2

     daytona_bug2_ioctl_example_2.bpl(1478,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2

     daytona_bug2_ioctl_example_2.bpl(1482,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2

     daytona_bug2_ioctl_example_2.bpl(1495,3): inline$dispatch$0$anon4_Else#2

@@ -164,30 +132,23 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1629,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2

     daytona_bug2_ioctl_example_2.bpl(1642,3): inline$I8xDeviceControl$0$anon16_Else#2

     daytona_bug2_ioctl_example_2.bpl(1655,3): inline$I8xDeviceControl$0$label_19_case_2#2

-    daytona_bug2_ioctl_example_2.bpl(1668,3): inline$I8xKeyboardGetSysButtonEvent$0$start#2

     daytona_bug2_ioctl_example_2.bpl(1719,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2

     daytona_bug2_ioctl_example_2.bpl(1723,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2

     daytona_bug2_ioctl_example_2.bpl(1736,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2

     daytona_bug2_ioctl_example_2.bpl(1749,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2

     daytona_bug2_ioctl_example_2.bpl(1757,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2

-    daytona_bug2_ioctl_example_2.bpl(1762,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23#2

-    daytona_bug2_ioctl_example_2.bpl(1768,3): inline$storm_KeAcquireSpinLock$0$Entry#2

     daytona_bug2_ioctl_example_2.bpl(1811,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1815,3): inline$storm_KeAcquireSpinLock$0$anon1#2

     daytona_bug2_ioctl_example_2.bpl(1835,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2

     daytona_bug2_ioctl_example_2.bpl(1843,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1847,3): inline$storm_KeAcquireSpinLock$0$anon4#2

     daytona_bug2_ioctl_example_2.bpl(1867,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2

     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(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(1906,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23$1#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

     daytona_bug2_ioctl_example_2.bpl(1951,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2

     daytona_bug2_ioctl_example_2.bpl(1991,3): inline$storm_IoSetCancelRoutine$0$label_8#2

-    daytona_bug2_ioctl_example_2.bpl(1995,3): inline$storm_IoSetCancelRoutine$0$label_16#2

     daytona_bug2_ioctl_example_2.bpl(2010,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2

     daytona_bug2_ioctl_example_2.bpl(2014,3): inline$storm_IoSetCancelRoutine$0$anon5#2

     daytona_bug2_ioctl_example_2.bpl(2034,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2

@@ -195,14 +156,12 @@ Execution trace:
     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(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(2072,3): inline$I8xKeyboardGetSysButtonEvent$0$label_62$1#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

     daytona_bug2_ioctl_example_2.bpl(2208,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2

     daytona_bug2_ioctl_example_2.bpl(2218,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2

     daytona_bug2_ioctl_example_2.bpl(2246,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2

     daytona_bug2_ioctl_example_2.bpl(2286,3): inline$storm_IoSetCancelRoutine$1$label_8#2

-    daytona_bug2_ioctl_example_2.bpl(2290,3): inline$storm_IoSetCancelRoutine$1$label_16#2

     daytona_bug2_ioctl_example_2.bpl(2293,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2

     daytona_bug2_ioctl_example_2.bpl(2301,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2

     daytona_bug2_ioctl_example_2.bpl(2311,3): inline$storm_IoSetCancelRoutine$1$anon5#2

@@ -212,18 +171,14 @@ Execution trace:
     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(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2

-    daytona_bug2_ioctl_example_2.bpl(2372,3): inline$I8xKeyboardGetSysButtonEvent$0$label_69$1#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

     daytona_bug2_ioctl_example_2.bpl(2407,3): inline$storm_IoMarkIrpPending$2$label_6_false#2

     daytona_bug2_ioctl_example_2.bpl(2447,3): inline$storm_IoMarkIrpPending$2$label_1#2

     daytona_bug2_ioctl_example_2.bpl(2454,3): inline$storm_IoMarkIrpPending$2$Return#2

-    daytona_bug2_ioctl_example_2.bpl(2457,3): inline$I8xKeyboardGetSysButtonEvent$0$label_73$1#2

     daytona_bug2_ioctl_example_2.bpl(2460,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2

     daytona_bug2_ioctl_example_2.bpl(2507,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2

-    daytona_bug2_ioctl_example_2.bpl(2514,3): inline$storm_KeReleaseSpinLock$0$Entry#2

     daytona_bug2_ioctl_example_2.bpl(2533,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2

-    daytona_bug2_ioctl_example_2.bpl(2537,3): inline$storm_KeReleaseSpinLock$0$anon1#2

     daytona_bug2_ioctl_example_2.bpl(2574,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2

     daytona_bug2_ioctl_example_2.bpl(2581,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2

     daytona_bug2_ioctl_example_2.bpl(2589,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2

@@ -231,7 +186,6 @@ Execution trace:
     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(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(2629,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59$1#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

     daytona_bug2_ioctl_example_2.bpl(2865,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2

@@ -241,23 +195,18 @@ Execution trace:
     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(2980,3): inline$storm_IoCompleteRequest$2$Return#2

-    daytona_bug2_ioctl_example_2.bpl(2983,3): inline$I8xCompleteSysButtonIrp$0$label_6$1#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(3003,3): inline$I8xKeyboardGetSysButtonEvent$0$label_53$1#2

     daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#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(3172,3): inline$I8xDeviceControl$0$label_24$1#2

     daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2

     daytona_bug2_ioctl_example_2.bpl(3644,3): inline$I8xDeviceControl$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(3655,3): inline$I8xDeviceControl$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(3658,3): inline$dispatch$0$label_8$1#2

     daytona_bug2_ioctl_example_2.bpl(3661,3): inline$dispatch$0$anon5_Else#2

     daytona_bug2_ioctl_example_2.bpl(3682,3): inline$dispatch$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(3685,3): label_23$1#2

     daytona_bug2_ioctl_example_2.bpl(3692,3): anon31_Then#2

-    daytona_bug2_ioctl_example_2.bpl(3705,3): label_27#2

+    daytona_bug2_ioctl_example_2.bpl(3697,3): anon17#2

     daytona_bug2_ioctl_example_2.bpl(3754,3): inline$storm_IoCancelIrp$0$anon23_Then#2

     daytona_bug2_ioctl_example_2.bpl(3759,3): inline$storm_IoCancelIrp$0$anon2#2

     daytona_bug2_ioctl_example_2.bpl(3783,3): inline$storm_IoCancelIrp$0$anon25_Then#2

@@ -266,137 +215,85 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(3814,3): inline$storm_IoCancelIrp$0$anon8#2

     daytona_bug2_ioctl_example_2.bpl(3825,3): inline$storm_IoCancelIrp$0$anon29_Then#2

     daytona_bug2_ioctl_example_2.bpl(3830,3): inline$storm_IoCancelIrp$0$anon10#2

-    daytona_bug2_ioctl_example_2.bpl(3834,3): inline$storm_IoCancelIrp$0$label_13#2

     daytona_bug2_ioctl_example_2.bpl(3890,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2

     daytona_bug2_ioctl_example_2.bpl(3900,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2

-    daytona_bug2_ioctl_example_2.bpl(3904,3): inline$storm_IoAcquireCancelSpinLock$0$anon2#2

     daytona_bug2_ioctl_example_2.bpl(3913,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2

     daytona_bug2_ioctl_example_2.bpl(3921,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2

     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(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(3961,3): inline$storm_IoCancelIrp$0$label_13$1#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

     daytona_bug2_ioctl_example_2.bpl(4000,3): inline$storm_IoCancelIrp$0$label_22_true#2

     daytona_bug2_ioctl_example_2.bpl(4008,3): inline$storm_IoCancelIrp$0$anon32_Else#2

-    daytona_bug2_ioctl_example_2.bpl(4012,3): inline$storm_IoCancelIrp$0$anon16#2

     daytona_bug2_ioctl_example_2.bpl(4021,3): inline$storm_IoCancelIrp$0$label_27_false#2

     daytona_bug2_ioctl_example_2.bpl(4722,3): inline$storm_IoCancelIrp$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(4741,3): inline$storm_IoCancelIrp$0$Return#2

-    daytona_bug2_ioctl_example_2.bpl(4744,3): inline$cancel$0$label_3$1#2

     daytona_bug2_ioctl_example_2.bpl(4757,3): inline$cancel$0$anon2_Then#2

     daytona_bug2_ioctl_example_2.bpl(4771,3): anon32_Then#2

-    daytona_bug2_ioctl_example_2.bpl(4784,3): label_31#2

+    daytona_bug2_ioctl_example_2.bpl(4776,3): anon19#2

     daytona_bug2_ioctl_example_2.bpl(4814,3): anon33_Then#2

-    daytona_bug2_ioctl_example_2.bpl(4824,3): label_1#2

+    daytona_bug2_ioctl_example_2.bpl(4819,3): anon21#2

 

 Boogie program verifier finished with 0 verified, 1 error

 stack_overflow.bpl(97942,5): Error BP5001: This assertion might not hold.

 Execution trace:

     stack_overflow.bpl(1141,3): start#1

-    stack_overflow.bpl(1163,3): label_8#1

-    stack_overflow.bpl(1168,3): label_9#1

     stack_overflow.bpl(1197,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1

-    stack_overflow.bpl(1205,3): inline$storm_IoAllocateIrp$0$label_13#1

-    stack_overflow.bpl(1216,3): inline$storm_IoAllocateIrp$0$label_18#1

-    stack_overflow.bpl(1221,3): inline$storm_IoAllocateIrp$0$label_19#1

     stack_overflow.bpl(1230,3): inline$storm_IoAllocateIrp$0$anon6_Else#1

-    stack_overflow.bpl(1234,3): inline$storm_IoAllocateIrp$0$anon1#1

-    stack_overflow.bpl(1238,3): inline$storm_IoAllocateIrp$0$label_21#1

-    stack_overflow.bpl(1242,3): inline$storm_IoAllocateIrp$0$label_22#1

     stack_overflow.bpl(1283,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1

     stack_overflow.bpl(1302,3): inline$storm_IoAllocateIrp$0$anon7_Else#1

     stack_overflow.bpl(1321,3): inline$storm_IoAllocateIrp$0$anon8_Else#1

     stack_overflow.bpl(1330,3): inline$storm_IoAllocateIrp$0$anon5#1

     stack_overflow.bpl(1350,3): inline$storm_IoAllocateIrp$0$label_36#1

-    stack_overflow.bpl(1354,3): inline$storm_IoAllocateIrp$0$label_1#1

     stack_overflow.bpl(1364,3): anon10_Else#1

     stack_overflow.bpl(1379,3): anon11_Else#1

-    stack_overflow.bpl(1383,3): anon3#1

     stack_overflow.bpl(1418,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1

     stack_overflow.bpl(1424,3): inline$IoSetNextIrpStackLocation$0$label_5#1

-    stack_overflow.bpl(1432,3): inline$IoSetNextIrpStackLocation$0$label_6#1

     stack_overflow.bpl(1446,3): anon12_Else#1

     stack_overflow.bpl(1486,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1

     stack_overflow.bpl(1507,3): anon13_Else#1

-    stack_overflow.bpl(1532,3): inline$myInitDriver$0$label_4#1

-    stack_overflow.bpl(1541,3): inline$myInitDriver$0$label_6#1

-    stack_overflow.bpl(1547,3): inline$storm_KeInitializeSpinLock$0$Entry#1

-    stack_overflow.bpl(1555,3): inline$storm_KeInitializeSpinLock$0$label_3#1

     stack_overflow.bpl(1569,3): inline$myInitDriver$0$anon8_Else#1

-    stack_overflow.bpl(1577,3): inline$myInitDriver$0$label_9#1

-    stack_overflow.bpl(1583,3): inline$storm_KeInitializeSpinLock$1$Entry#1

-    stack_overflow.bpl(1591,3): inline$storm_KeInitializeSpinLock$1$label_3#1

     stack_overflow.bpl(1605,3): inline$myInitDriver$0$anon9_Else#1

-    stack_overflow.bpl(1613,3): inline$myInitDriver$0$label_12#1

-    stack_overflow.bpl(1619,3): inline$storm_KeInitializeSpinLock$2$Entry#1

-    stack_overflow.bpl(1627,3): inline$storm_KeInitializeSpinLock$2$label_3#1

     stack_overflow.bpl(1641,3): inline$myInitDriver$0$anon10_Else#1

-    stack_overflow.bpl(1649,3): inline$myInitDriver$0$label_15#1

-    stack_overflow.bpl(1655,3): inline$storm_KeInitializeSpinLock$3$Entry#1

-    stack_overflow.bpl(1663,3): inline$storm_KeInitializeSpinLock$3$label_3#1

     stack_overflow.bpl(1677,3): inline$myInitDriver$0$anon11_Else#1

     stack_overflow.bpl(1704,3): inline$myInitDriver$0$Return#1

-    stack_overflow.bpl(1707,3): label_23$1#1

     stack_overflow.bpl(1710,3): anon14_Else#1

-    stack_overflow.bpl(1729,3): inline$storm_thread_dispatch$0$start#1

     stack_overflow.bpl(1773,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1

     stack_overflow.bpl(1794,3): inline$storm_thread_dispatch$0$anon4_Else#1

-    stack_overflow.bpl(1827,3): inline$BDLPnP$0$label_6#1

     stack_overflow.bpl(1877,3): inline$BDLPnP$0$anon54_Else#1

     stack_overflow.bpl(1891,3): inline$BDLPnP$0$label_16_true#1

-    stack_overflow.bpl(1895,3): inline$BDLPnP$0$label_20#1

-    stack_overflow.bpl(1899,3): inline$BDLPnP$0$label_21#1

-    stack_overflow.bpl(1903,3): inline$BDLPnP$0$label_22#1

     stack_overflow.bpl(1935,3): inline$BDLPnP$0$anon55_Else#1

     stack_overflow.bpl(1949,3): inline$BDLPnP$0$label_26_true#1

-    stack_overflow.bpl(1953,3): inline$BDLPnP$0$label_30#1

-    stack_overflow.bpl(1957,3): inline$BDLPnP$0$label_31#1

-    stack_overflow.bpl(1961,3): inline$BDLPnP$0$label_32#1

     stack_overflow.bpl(1993,3): inline$BDLPnP$0$anon56_Else#1

     stack_overflow.bpl(2007,3): inline$BDLPnP$0$label_36_true#1

     stack_overflow.bpl(2052,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1

     stack_overflow.bpl(2073,3): inline$BDLPnP$0$anon57_Else#1

-    stack_overflow.bpl(2083,3): inline$BDLPnP$0$label_43#1

     stack_overflow.bpl(2100,3): inline$BDLPnP$0$label_44_true#1

     stack_overflow.bpl(2109,3): inline$BDLPnP$0$label_47#1

     stack_overflow.bpl(2113,3): inline$BDLPnP$0$anon58_Else#1

     stack_overflow.bpl(2127,3): inline$BDLPnP$0$label_51_false#1

     stack_overflow.bpl(77682,3): inline$BDLPnP$0$label_52_case_1#1

-    stack_overflow.bpl(77695,3): inline$BDLPnPStart$0$start#1

     stack_overflow.bpl(77742,3): inline$BDLPnPStart$0$anon36_Else#1

     stack_overflow.bpl(77756,3): inline$BDLPnPStart$0$label_11_true#1

-    stack_overflow.bpl(77760,3): inline$BDLPnPStart$0$label_15#1

-    stack_overflow.bpl(77764,3): inline$BDLPnPStart$0$label_16#1

-    stack_overflow.bpl(77768,3): inline$BDLPnPStart$0$label_17#1

     stack_overflow.bpl(77800,3): inline$BDLPnPStart$0$anon37_Else#1

     stack_overflow.bpl(77814,3): inline$BDLPnPStart$0$label_21_true#1

-    stack_overflow.bpl(77818,3): inline$BDLPnPStart$0$label_25#1

-    stack_overflow.bpl(77822,3): inline$BDLPnPStart$0$label_26#1

-    stack_overflow.bpl(77826,3): inline$BDLPnPStart$0$label_27#1

     stack_overflow.bpl(77858,3): inline$BDLPnPStart$0$anon38_Else#1

     stack_overflow.bpl(77872,3): inline$BDLPnPStart$0$label_31_true#1

-    stack_overflow.bpl(77886,3): inline$BDLCallLowerLevelDriverAndWait$0$start#1

+    stack_overflow.bpl(77879,3): inline$BDLPnPStart$0$label_32#1

     stack_overflow.bpl(77951,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1

     stack_overflow.bpl(77972,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1

     stack_overflow.bpl(78013,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1

     stack_overflow.bpl(78032,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1

     stack_overflow.bpl(78060,3): inline$IoCopyCurrentIrpStackLocationToNext$0$Return#1

-    stack_overflow.bpl(78063,3): inline$BDLCallLowerLevelDriverAndWait$0$label_6$1#1

     stack_overflow.bpl(78066,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1

-    stack_overflow.bpl(78086,3): inline$storm_KeInitializeEvent$0$label_3#1

     stack_overflow.bpl(78100,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1

     stack_overflow.bpl(78128,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1

     stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1

-    stack_overflow.bpl(78170,3): inline$IoGetNextIrpStackLocation$2$Entry#1

-    stack_overflow.bpl(78174,3): inline$IoGetNextIrpStackLocation$2$start#1

-    stack_overflow.bpl(78178,3): inline$IoGetNextIrpStackLocation$2$label_3#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(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1

-    stack_overflow.bpl(78247,3): inline$BDLCallLowerLevelDriverAndWait$0$label_12$1#1

     stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1

     stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1

     stack_overflow.bpl(78311,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1

@@ -404,37 +301,24 @@ Execution trace:
     stack_overflow.bpl(83288,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1

     stack_overflow.bpl(83333,3): inline$storm_IoCallDriver$1$label_9_false#1

     stack_overflow.bpl(83372,3): inline$storm_IoCallDriver$1$label_10#1

-    stack_overflow.bpl(83375,3): inline$IoSetNextIrpStackLocation$2$Entry#1

-    stack_overflow.bpl(83379,3): inline$IoSetNextIrpStackLocation$2$start#1

-    stack_overflow.bpl(83383,3): inline$IoSetNextIrpStackLocation$2$label_3#1

     stack_overflow.bpl(83403,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1

     stack_overflow.bpl(83409,3): inline$IoSetNextIrpStackLocation$2$label_5#1

-    stack_overflow.bpl(83417,3): inline$IoSetNextIrpStackLocation$2$label_6#1

     stack_overflow.bpl(83431,3): inline$storm_IoCallDriver$1$anon11_Else#1

     stack_overflow.bpl(83471,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1

     stack_overflow.bpl(83492,3): inline$storm_IoCallDriver$1$anon13_Else#1

-    stack_overflow.bpl(83505,3): inline$storm_IoCallDriver$1$label_23#1

     stack_overflow.bpl(85859,3): inline$storm_IoCallDriver$1$label_27_case_1#1

     stack_overflow.bpl(85929,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1

     stack_overflow.bpl(85950,3): inline$CallCompletionRoutine$3$anon10_Else#1

     stack_overflow.bpl(86007,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1

     stack_overflow.bpl(86028,3): inline$CallCompletionRoutine$3$anon11_Else#1

     stack_overflow.bpl(86045,3): inline$CallCompletionRoutine$3$label_18_true#1

-    stack_overflow.bpl(86049,3): inline$CallCompletionRoutine$3$label_19#1

     stack_overflow.bpl(87162,3): inline$CallCompletionRoutine$3$label_20_icall_2#1

-    stack_overflow.bpl(87173,3): inline$BDLDevicePowerIoCompletion$3$start#1

     stack_overflow.bpl(87239,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1

     stack_overflow.bpl(87262,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1

     stack_overflow.bpl(87307,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1

     stack_overflow.bpl(87321,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1

-    stack_overflow.bpl(87325,3): inline$BDLDevicePowerIoCompletion$3$label_24#1

-    stack_overflow.bpl(87329,3): inline$BDLDevicePowerIoCompletion$3$label_25#1

-    stack_overflow.bpl(87333,3): inline$BDLDevicePowerIoCompletion$3$label_26#1

     stack_overflow.bpl(87365,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1

     stack_overflow.bpl(87379,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1

-    stack_overflow.bpl(87383,3): inline$BDLDevicePowerIoCompletion$3$label_34#1

-    stack_overflow.bpl(87387,3): inline$BDLDevicePowerIoCompletion$3$label_35#1

-    stack_overflow.bpl(87391,3): inline$BDLDevicePowerIoCompletion$3$label_36#1

     stack_overflow.bpl(87423,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1

     stack_overflow.bpl(87437,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1

     stack_overflow.bpl(87452,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1

@@ -442,14 +326,8 @@ Execution trace:
     stack_overflow.bpl(87527,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1

     stack_overflow.bpl(87555,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1

     stack_overflow.bpl(87569,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1

-    stack_overflow.bpl(87573,3): inline$BDLDevicePowerIoCompletion$3$label_66#1

-    stack_overflow.bpl(87577,3): inline$BDLDevicePowerIoCompletion$3$label_67#1

-    stack_overflow.bpl(87581,3): inline$BDLDevicePowerIoCompletion$3$label_68#1

     stack_overflow.bpl(87613,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1

     stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1

-    stack_overflow.bpl(87631,3): inline$BDLDevicePowerIoCompletion$3$label_76#1

-    stack_overflow.bpl(87635,3): inline$BDLDevicePowerIoCompletion$3$label_77#1

-    stack_overflow.bpl(87639,3): inline$BDLDevicePowerIoCompletion$3$label_78#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(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1

@@ -458,103 +336,63 @@ Execution trace:
     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(87789,3): inline$storm_IoCompleteRequest$7$Return#1

-    stack_overflow.bpl(87792,3): inline$BDLDevicePowerIoCompletion$3$label_92$1#1

     stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1

     stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1

     stack_overflow.bpl(87837,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1

     stack_overflow.bpl(87851,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1

-    stack_overflow.bpl(87855,3): inline$BDLDevicePowerIoCompletion$3$label_105#1

-    stack_overflow.bpl(87859,3): inline$BDLDevicePowerIoCompletion$3$label_106#1

-    stack_overflow.bpl(87863,3): inline$BDLDevicePowerIoCompletion$3$label_107#1

     stack_overflow.bpl(87895,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1

     stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1

-    stack_overflow.bpl(87913,3): inline$BDLDevicePowerIoCompletion$3$label_115#1

-    stack_overflow.bpl(87917,3): inline$BDLDevicePowerIoCompletion$3$label_116#1

-    stack_overflow.bpl(87921,3): inline$BDLDevicePowerIoCompletion$3$label_117#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(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1

-    stack_overflow.bpl(88043,3): inline$CallCompletionRoutine$3$label_20_icall_2$1#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(88149,3): inline$CallCompletionRoutine$3$label_23#1

-    stack_overflow.bpl(88153,3): inline$CallCompletionRoutine$3$label_24#1

     stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1

-    stack_overflow.bpl(88164,3): inline$CallCompletionRoutine$3$label_25#1

     stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1

-    stack_overflow.bpl(88187,3): inline$storm_IoCallDriver$1$label_39$1#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(88237,3): inline$storm_IoCallDriver$1$Return#1

-    stack_overflow.bpl(88241,3): inline$storm_PoCallDriver$0$label_3$1#1

     stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1

     stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1

-    stack_overflow.bpl(88266,3): inline$BDLCallLowerLevelDriverAndWait$0$label_25$1#1

     stack_overflow.bpl(88269,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1

     stack_overflow.bpl(88283,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1

     stack_overflow.bpl(88441,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1

-    stack_overflow.bpl(88445,3): inline$BDLCallLowerLevelDriverAndWait$0$label_1#1

     stack_overflow.bpl(88477,3): inline$BDLCallLowerLevelDriverAndWait$0$Return#1

-    stack_overflow.bpl(88481,3): inline$BDLPnPStart$0$label_32$1#1

     stack_overflow.bpl(88484,3): inline$BDLPnPStart$0$anon39_Else#1

     stack_overflow.bpl(88675,3): inline$BDLPnPStart$0$label_37_true#1

     stack_overflow.bpl(88987,3): inline$BDLPnPStart$0$label_51_true#1

     stack_overflow.bpl(89015,3): inline$BDLPnPStart$0$anon41_Else#1

     stack_overflow.bpl(89029,3): inline$BDLPnPStart$0$label_56_true#1

-    stack_overflow.bpl(89033,3): inline$BDLPnPStart$0$label_60#1

-    stack_overflow.bpl(89037,3): inline$BDLPnPStart$0$label_61#1

-    stack_overflow.bpl(89041,3): inline$BDLPnPStart$0$label_62#1

     stack_overflow.bpl(89073,3): inline$BDLPnPStart$0$anon42_Else#1

     stack_overflow.bpl(89087,3): inline$BDLPnPStart$0$label_66_true#1

-    stack_overflow.bpl(89091,3): inline$BDLPnPStart$0$label_70#1

-    stack_overflow.bpl(89095,3): inline$BDLPnPStart$0$label_71#1

-    stack_overflow.bpl(89099,3): inline$BDLPnPStart$0$label_72#1

     stack_overflow.bpl(89131,3): inline$BDLPnPStart$0$anon43_Else#1

     stack_overflow.bpl(89145,3): inline$BDLPnPStart$0$label_76_true#1

     stack_overflow.bpl(89176,3): inline$BDLPnPStart$0$anon44_Else#1

     stack_overflow.bpl(89190,3): inline$BDLPnPStart$0$label_81_true#1

-    stack_overflow.bpl(89194,3): inline$BDLPnPStart$0$label_85#1

-    stack_overflow.bpl(89198,3): inline$BDLPnPStart$0$label_86#1

-    stack_overflow.bpl(89202,3): inline$BDLPnPStart$0$label_87#1

     stack_overflow.bpl(89234,3): inline$BDLPnPStart$0$anon45_Else#1

     stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1

-    stack_overflow.bpl(89252,3): inline$BDLPnPStart$0$label_95#1

-    stack_overflow.bpl(89256,3): inline$BDLPnPStart$0$label_96#1

-    stack_overflow.bpl(89260,3): inline$BDLPnPStart$0$label_97#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(89361,3): inline$BDLPnPStart$0$Return#1

-    stack_overflow.bpl(89365,3): inline$BDLPnP$0$label_113$1#1

     stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1

     stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1

     stack_overflow.bpl(94593,3): inline$BDLPnP$0$label_139_true#1

     stack_overflow.bpl(94622,3): inline$storm_IoCompleteRequest$57$label_6_true#1

     stack_overflow.bpl(94630,3): inline$storm_IoCompleteRequest$57$anon3_Else#1

-    stack_overflow.bpl(94634,3): inline$storm_IoCompleteRequest$57$anon1#1

     stack_overflow.bpl(94642,3): inline$storm_IoCompleteRequest$57$label_9_false#1

     stack_overflow.bpl(94662,3): inline$storm_IoCompleteRequest$57$label_1#1

     stack_overflow.bpl(94669,3): inline$storm_IoCompleteRequest$57$Return#1

-    stack_overflow.bpl(94672,3): inline$BDLPnP$0$label_142$1#1

     stack_overflow.bpl(94710,3): inline$BDLPnP$0$anon75_Then#1

     stack_overflow.bpl(95206,3): inline$BDLPnP$0$Return#1

-    stack_overflow.bpl(95209,3): inline$storm_thread_dispatch$0$label_8$1#1

     stack_overflow.bpl(95226,3): inline$storm_thread_dispatch$0$anon5_Then#1

     stack_overflow.bpl(95234,3): inline$storm_thread_dispatch$0$Return#1

-    stack_overflow.bpl(95237,3): label_29$1#1

-    stack_overflow.bpl(95240,3): label_32#1

-    stack_overflow.bpl(95243,3): inline$storm_thread_cancel$0$Entry#1

-    stack_overflow.bpl(95247,3): inline$storm_thread_cancel$0$start#1

-    stack_overflow.bpl(95276,3): inline$storm_IoCancelIrp$0$label_8#1

-    stack_overflow.bpl(95282,3): inline$storm_IoCancelIrp$0$label_9#1

     stack_overflow.bpl(95294,3): inline$storm_IoCancelIrp$0$anon9_Then#1

     stack_overflow.bpl(95299,3): inline$storm_IoCancelIrp$0$anon1#1

-    stack_overflow.bpl(95303,3): inline$storm_IoCancelIrp$0$label_13#1

     stack_overflow.bpl(95356,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1

     stack_overflow.bpl(95518,3): inline$storm_IoCancelIrp$0$anon10_Then#1

     stack_overflow.bpl(95539,3): inline$storm_thread_cancel$0$anon2_Then#1

-    stack_overflow.bpl(95555,3): inline$storm_thread_dpc$0$start#1

-    stack_overflow.bpl(95578,3): inline$storm_thread_completion$0$start#1

+    stack_overflow.bpl(95543,3): inline$storm_thread_cancel$0$Return#1

     stack_overflow.bpl(97931,3): inline$storm_thread_completion$0$anon4_Then#1

-    stack_overflow.bpl(97941,3): label_1#1

+    stack_overflow.bpl(97935,3): inline$storm_thread_completion$0$Return#1

 

 Boogie program verifier finished with 0 verified, 1 error