stack_overflow.bpl(97944,5): Error BP5001: This assertion might not hold.
Execution trace:
    stack_overflow.bpl(1143,3): start#1
    stack_overflow.bpl(1199,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
    stack_overflow.bpl(1232,3): inline$storm_IoAllocateIrp$0$anon6_Else#1
    stack_overflow.bpl(1285,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1
    stack_overflow.bpl(1304,3): inline$storm_IoAllocateIrp$0$anon7_Else#1
    stack_overflow.bpl(1323,3): inline$storm_IoAllocateIrp$0$anon8_Else#1
    stack_overflow.bpl(1332,3): inline$storm_IoAllocateIrp$0$anon5#1
    stack_overflow.bpl(1352,3): inline$storm_IoAllocateIrp$0$label_36#1
    stack_overflow.bpl(1366,3): anon10_Else#1
    stack_overflow.bpl(1381,3): anon11_Else#1
    stack_overflow.bpl(1420,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1
    stack_overflow.bpl(1426,3): inline$IoSetNextIrpStackLocation$0$label_5#1
    stack_overflow.bpl(1448,3): anon12_Else#1
    stack_overflow.bpl(1488,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1
    stack_overflow.bpl(1509,3): anon13_Else#1
    stack_overflow.bpl(1571,3): inline$myInitDriver$0$anon8_Else#1
    stack_overflow.bpl(1607,3): inline$myInitDriver$0$anon9_Else#1
    stack_overflow.bpl(1643,3): inline$myInitDriver$0$anon10_Else#1
    stack_overflow.bpl(1679,3): inline$myInitDriver$0$anon11_Else#1
    stack_overflow.bpl(1712,3): anon14_Else#1
    stack_overflow.bpl(1775,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1
    stack_overflow.bpl(1796,3): inline$storm_thread_dispatch$0$anon4_Else#1
    stack_overflow.bpl(1879,3): inline$BDLPnP$0$anon54_Else#1
    stack_overflow.bpl(1893,3): inline$BDLPnP$0$label_16_true#1
    stack_overflow.bpl(1937,3): inline$BDLPnP$0$anon55_Else#1
    stack_overflow.bpl(1951,3): inline$BDLPnP$0$label_26_true#1
    stack_overflow.bpl(1995,3): inline$BDLPnP$0$anon56_Else#1
    stack_overflow.bpl(2009,3): inline$BDLPnP$0$label_36_true#1
    stack_overflow.bpl(2054,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1
    stack_overflow.bpl(2075,3): inline$BDLPnP$0$anon57_Else#1
    stack_overflow.bpl(2102,3): inline$BDLPnP$0$label_44_true#1
    stack_overflow.bpl(2111,3): inline$BDLPnP$0$label_47#1
    stack_overflow.bpl(2115,3): inline$BDLPnP$0$anon58_Else#1
    stack_overflow.bpl(2129,3): inline$BDLPnP$0$label_51_false#1
    stack_overflow.bpl(77684,3): inline$BDLPnP$0$label_52_case_1#1
    stack_overflow.bpl(77744,3): inline$BDLPnPStart$0$anon36_Else#1
    stack_overflow.bpl(77758,3): inline$BDLPnPStart$0$label_11_true#1
    stack_overflow.bpl(77802,3): inline$BDLPnPStart$0$anon37_Else#1
    stack_overflow.bpl(77816,3): inline$BDLPnPStart$0$label_21_true#1
    stack_overflow.bpl(77860,3): inline$BDLPnPStart$0$anon38_Else#1
    stack_overflow.bpl(77874,3): inline$BDLPnPStart$0$label_31_true#1
    stack_overflow.bpl(77881,3): inline$BDLPnPStart$0$label_32#1
    stack_overflow.bpl(77953,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1
    stack_overflow.bpl(77974,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1
    stack_overflow.bpl(78015,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1
    stack_overflow.bpl(78034,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1
    stack_overflow.bpl(78068,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1
    stack_overflow.bpl(78102,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1
    stack_overflow.bpl(78130,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1
    stack_overflow.bpl(78200,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
    stack_overflow.bpl(78219,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
    stack_overflow.bpl(78235,3): inline$storm_IoSetCompletionRoutine$0$label_1#1
    stack_overflow.bpl(78252,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
    stack_overflow.bpl(78292,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
    stack_overflow.bpl(78313,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1
    stack_overflow.bpl(83281,3): inline$BDLCallLowerLevelDriverAndWait$0$label_18_true#1
    stack_overflow.bpl(83290,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1
    stack_overflow.bpl(83335,3): inline$storm_IoCallDriver$1$label_9_false#1
    stack_overflow.bpl(83405,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1
    stack_overflow.bpl(83411,3): inline$IoSetNextIrpStackLocation$2$label_5#1
    stack_overflow.bpl(83433,3): inline$storm_IoCallDriver$1$anon11_Else#1
    stack_overflow.bpl(83473,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1
    stack_overflow.bpl(83494,3): inline$storm_IoCallDriver$1$anon13_Else#1
    stack_overflow.bpl(85861,3): inline$storm_IoCallDriver$1$label_27_case_1#1
    stack_overflow.bpl(85931,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1
    stack_overflow.bpl(85952,3): inline$CallCompletionRoutine$3$anon10_Else#1
    stack_overflow.bpl(86009,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1
    stack_overflow.bpl(86030,3): inline$CallCompletionRoutine$3$anon11_Else#1
    stack_overflow.bpl(86047,3): inline$CallCompletionRoutine$3$label_18_true#1
    stack_overflow.bpl(87164,3): inline$CallCompletionRoutine$3$label_20_icall_2#1
    stack_overflow.bpl(87241,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1
    stack_overflow.bpl(87264,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1
    stack_overflow.bpl(87309,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1
    stack_overflow.bpl(87323,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1
    stack_overflow.bpl(87367,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1
    stack_overflow.bpl(87381,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1
    stack_overflow.bpl(87425,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1
    stack_overflow.bpl(87439,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1
    stack_overflow.bpl(87454,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1
    stack_overflow.bpl(87485,3): inline$BDLDevicePowerIoCompletion$3$label_44_true#1
    stack_overflow.bpl(87529,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1
    stack_overflow.bpl(87557,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1
    stack_overflow.bpl(87571,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1
    stack_overflow.bpl(87615,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1
    stack_overflow.bpl(87629,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
    stack_overflow.bpl(87673,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
    stack_overflow.bpl(87687,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
    stack_overflow.bpl(87694,3): inline$BDLDevicePowerIoCompletion$3$label_83#1
    stack_overflow.bpl(87700,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
    stack_overflow.bpl(87704,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1
    stack_overflow.bpl(87715,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1
    stack_overflow.bpl(87740,3): inline$storm_IoCompleteRequest$7$label_6_false#1
    stack_overflow.bpl(87779,3): inline$storm_IoCompleteRequest$7$label_7#1
    stack_overflow.bpl(87784,3): inline$storm_IoCompleteRequest$7$label_1#1
    stack_overflow.bpl(87797,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
    stack_overflow.bpl(87808,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
    stack_overflow.bpl(87839,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1
    stack_overflow.bpl(87853,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1
    stack_overflow.bpl(87897,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1
    stack_overflow.bpl(87911,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
    stack_overflow.bpl(87955,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
    stack_overflow.bpl(87969,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
    stack_overflow.bpl(87976,3): inline$BDLDevicePowerIoCompletion$3$label_122#1
    stack_overflow.bpl(88048,3): inline$CallCompletionRoutine$3$anon13_Else#1
    stack_overflow.bpl(88162,3): inline$CallCompletionRoutine$3$label_24_true#1
    stack_overflow.bpl(88171,3): inline$CallCompletionRoutine$3$label_1#1
    stack_overflow.bpl(88192,3): inline$storm_IoCallDriver$1$anon15_Else#1
    stack_overflow.bpl(88220,3): inline$storm_IoCallDriver$1$label_36#1
    stack_overflow.bpl(88224,3): inline$storm_IoCallDriver$1$label_1#1
    stack_overflow.bpl(88246,3): inline$storm_PoCallDriver$0$anon2_Else#1
    stack_overflow.bpl(88271,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1
    stack_overflow.bpl(88285,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1
    stack_overflow.bpl(88443,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1
    stack_overflow.bpl(88486,3): inline$BDLPnPStart$0$anon39_Else#1
    stack_overflow.bpl(88677,3): inline$BDLPnPStart$0$label_37_true#1
    stack_overflow.bpl(88989,3): inline$BDLPnPStart$0$label_51_true#1
    stack_overflow.bpl(89017,3): inline$BDLPnPStart$0$anon41_Else#1
    stack_overflow.bpl(89031,3): inline$BDLPnPStart$0$label_56_true#1
    stack_overflow.bpl(89075,3): inline$BDLPnPStart$0$anon42_Else#1
    stack_overflow.bpl(89089,3): inline$BDLPnPStart$0$label_66_true#1
    stack_overflow.bpl(89133,3): inline$BDLPnPStart$0$anon43_Else#1
    stack_overflow.bpl(89147,3): inline$BDLPnPStart$0$label_76_true#1
    stack_overflow.bpl(89178,3): inline$BDLPnPStart$0$anon44_Else#1
    stack_overflow.bpl(89192,3): inline$BDLPnPStart$0$label_81_true#1
    stack_overflow.bpl(89236,3): inline$BDLPnPStart$0$anon45_Else#1
    stack_overflow.bpl(89250,3): inline$BDLPnPStart$0$label_91_true#1
    stack_overflow.bpl(89294,3): inline$BDLPnPStart$0$anon46_Else#1
    stack_overflow.bpl(89308,3): inline$BDLPnPStart$0$label_101_true#1
    stack_overflow.bpl(89315,3): inline$BDLPnPStart$0$label_102#1
    stack_overflow.bpl(89370,3): inline$BDLPnP$0$anon67_Else#1
    stack_overflow.bpl(94595,3): inline$BDLPnP$0$label_139_true#1
    stack_overflow.bpl(94624,3): inline$storm_IoCompleteRequest$57$label_6_true#1
    stack_overflow.bpl(94632,3): inline$storm_IoCompleteRequest$57$anon3_Else#1
    stack_overflow.bpl(94644,3): inline$storm_IoCompleteRequest$57$label_9_false#1
    stack_overflow.bpl(94664,3): inline$storm_IoCompleteRequest$57$label_1#1
    stack_overflow.bpl(94712,3): inline$BDLPnP$0$anon75_Then#1
    stack_overflow.bpl(95228,3): inline$storm_thread_dispatch$0$anon5_Then#1
    stack_overflow.bpl(95236,3): inline$storm_thread_dispatch$0$Return#1
    stack_overflow.bpl(95296,3): inline$storm_IoCancelIrp$0$anon9_Then#1
    stack_overflow.bpl(95301,3): inline$storm_IoCancelIrp$0$anon1#1
    stack_overflow.bpl(95358,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1
    stack_overflow.bpl(95520,3): inline$storm_IoCancelIrp$0$anon10_Then#1
    stack_overflow.bpl(95541,3): inline$storm_thread_cancel$0$anon2_Then#1
    stack_overflow.bpl(95545,3): inline$storm_thread_cancel$0$Return#1
    stack_overflow.bpl(97933,3): inline$storm_thread_completion$0$anon4_Then#1
    stack_overflow.bpl(97937,3): inline$storm_thread_completion$0$Return#1

Boogie program verifier finished with 0 verified, 1 error