1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
bla1.bpl(2097,5): Error BP5001: This assertion might not hold.
Execution trace:
bla1.bpl(751,3): start#1
bla1.bpl(791,3): anon10_Then#1
bla1.bpl(796,3): anon2#1
bla1.bpl(824,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
bla1.bpl(856,3): inline$storm_IoAllocateIrp$0$anon14_Then#1
bla1.bpl(861,3): inline$storm_IoAllocateIrp$0$anon2#1
bla1.bpl(881,3): inline$storm_IoAllocateIrp$0$anon16_Then#1
bla1.bpl(886,3): inline$storm_IoAllocateIrp$0$anon5#1
bla1.bpl(906,3): inline$storm_IoAllocateIrp$0$anon18_Then#1
bla1.bpl(911,3): inline$storm_IoAllocateIrp$0$anon8#1
bla1.bpl(947,3): inline$storm_IoAllocateIrp$0$anon20_Then#1
bla1.bpl(952,3): inline$storm_IoAllocateIrp$0$anon11#1
bla1.bpl(983,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1
bla1.bpl(988,3): inline$IoGetNextIrpStackLocation$0$anon2#1
bla1.bpl(1020,3): inline$storm_IoAllocateIrp$0$anon22_Then#1
bla1.bpl(1025,3): inline$storm_IoAllocateIrp$0$anon13#1
bla1.bpl(1037,3): inline$storm_IoAllocateIrp$0$label_36#1
bla1.bpl(1091,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1
bla1.bpl(1096,3): inline$IoSetNextIrpStackLocation$0$anon2#1
bla1.bpl(1114,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1
bla1.bpl(1119,3): inline$IoSetNextIrpStackLocation$0$anon5#1
bla1.bpl(1159,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#1
bla1.bpl(1164,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1
bla1.bpl(1199,3): anon12_Then#1
bla1.bpl(1204,3): anon5#1
bla1.bpl(1257,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1
bla1.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1
bla1.bpl(1310,3): inline$I8xDeviceControl$0$anon3_Then#1
bla1.bpl(1314,3): inline$I8xDeviceControl$0$anon2#1
bla1.bpl(1350,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1
bla1.bpl(1378,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1
bla1.bpl(1429,3): inline$storm_IoSetCancelRoutine$0$anon9_Then#1
bla1.bpl(1433,3): inline$storm_IoSetCancelRoutine$0$anon3#1
bla1.bpl(1453,3): inline$storm_IoSetCancelRoutine$0$anon11_Then#1
bla1.bpl(1458,3): inline$storm_IoSetCancelRoutine$0$anon6#1
bla1.bpl(1469,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1
bla1.bpl(1474,3): inline$storm_IoSetCancelRoutine$0$anon8#1
bla1.bpl(1526,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1
bla1.bpl(1534,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1
bla1.bpl(1544,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1
bla1.bpl(1568,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1
bla1.bpl(1588,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1
bla1.bpl(1621,3): inline$storm_IoCompleteRequest$0$label_6_false#1
bla1.bpl(1656,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
bla1.bpl(1664,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
bla1.bpl(1674,3): inline$storm_IoCompleteRequest$0$anon2#1
bla1.bpl(1678,3): inline$storm_IoCompleteRequest$0$label_1#1
bla1.bpl(1736,3): anon14_Then#1
bla1.bpl(1741,3): anon7#1
bla1.bpl(1798,3): inline$storm_IoCancelIrp$0$anon12_Then#1
bla1.bpl(1803,3): inline$storm_IoCancelIrp$0$anon2#1
bla1.bpl(1827,3): inline$storm_IoCancelIrp$0$anon14_Then#1
bla1.bpl(1832,3): inline$storm_IoCancelIrp$0$anon5#1
bla1.bpl(1853,3): inline$storm_IoCancelIrp$0$anon16_Then#1
bla1.bpl(1858,3): inline$storm_IoCancelIrp$0$anon8#1
bla1.bpl(1869,3): inline$storm_IoCancelIrp$0$anon18_Then#1
bla1.bpl(1874,3): inline$storm_IoCancelIrp$0$anon10#1
bla1.bpl(1934,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1
bla1.bpl(1962,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1
bla1.bpl(1967,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1
bla1.bpl(1978,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1
bla1.bpl(1983,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1
bla1.bpl(2007,3): inline$storm_IoCancelIrp$0$label_16_true#1
bla1.bpl(2025,3): inline$storm_IoCancelIrp$0$label_22_true#1
bla1.bpl(2038,3): inline$storm_IoCancelIrp$0$label_25_false#1
bla1.bpl(2078,3): anon15_Then#1
bla1.bpl(2083,3): anon9#1
Boogie program verifier finished with 0 verified, 1 error
|
