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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
daytona_bug2_ioctl_example_2.bpl(4835,5): Error BP5001: This assertion might not hold.
Execution trace:
daytona_bug2_ioctl_example_2.bpl(807,3): start#2
daytona_bug2_ioctl_example_2.bpl(848,3): anon22_Then#2
daytona_bug2_ioctl_example_2.bpl(853,3): anon2#2
daytona_bug2_ioctl_example_2.bpl(881,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2
daytona_bug2_ioctl_example_2.bpl(913,3): inline$storm_IoAllocateIrp$0$anon18_Then#2
daytona_bug2_ioctl_example_2.bpl(918,3): inline$storm_IoAllocateIrp$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(938,3): inline$storm_IoAllocateIrp$0$anon20_Then#2
daytona_bug2_ioctl_example_2.bpl(943,3): inline$storm_IoAllocateIrp$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(963,3): inline$storm_IoAllocateIrp$0$anon22_Then#2
daytona_bug2_ioctl_example_2.bpl(968,3): inline$storm_IoAllocateIrp$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(976,3): inline$storm_IoAllocateIrp$0$anon24_Else#2
daytona_bug2_ioctl_example_2.bpl(1012,3): inline$storm_IoAllocateIrp$0$anon25_Then#2
daytona_bug2_ioctl_example_2.bpl(1017,3): inline$storm_IoAllocateIrp$0$anon13#2
daytona_bug2_ioctl_example_2.bpl(1048,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1053,3): inline$IoGetNextIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1068,3): inline$storm_IoAllocateIrp$0$anon27_Else#2
daytona_bug2_ioctl_example_2.bpl(1092,3): inline$storm_IoAllocateIrp$0$anon28_Then#2
daytona_bug2_ioctl_example_2.bpl(1097,3): inline$storm_IoAllocateIrp$0$anon17#2
daytona_bug2_ioctl_example_2.bpl(1117,3): inline$storm_IoAllocateIrp$0$label_36#2
daytona_bug2_ioctl_example_2.bpl(1131,3): anon24_Else#2
daytona_bug2_ioctl_example_2.bpl(1146,3): anon25_Else#2
daytona_bug2_ioctl_example_2.bpl(1186,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2
daytona_bug2_ioctl_example_2.bpl(1191,3): inline$IoSetNextIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1209,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2
daytona_bug2_ioctl_example_2.bpl(1214,3): inline$IoSetNextIrpStackLocation$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(1227,3): anon26_Else#2
daytona_bug2_ioctl_example_2.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1266,3): inline$IoGetCurrentIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1281,3): anon27_Else#2
daytona_bug2_ioctl_example_2.bpl(1308,3): anon28_Then#2
daytona_bug2_ioctl_example_2.bpl(1313,3): anon13#2
daytona_bug2_ioctl_example_2.bpl(1345,3): inline$myInitDriver$0$anon5_Then#2
daytona_bug2_ioctl_example_2.bpl(1350,3): inline$myInitDriver$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1385,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1390,3): inline$storm_KeInitializeSpinLock$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1403,3): inline$myInitDriver$0$anon7_Else#2
daytona_bug2_ioctl_example_2.bpl(1424,3): anon30_Else#2
daytona_bug2_ioctl_example_2.bpl(1480,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1484,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2
daytona_bug2_ioctl_example_2.bpl(1497,3): inline$dispatch$0$anon4_Else#2
daytona_bug2_ioctl_example_2.bpl(1536,3): inline$I8xDeviceControl$0$anon13_Else#2
daytona_bug2_ioctl_example_2.bpl(1559,3): inline$I8xDeviceControl$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1564,3): inline$I8xDeviceControl$0$anon4#2
daytona_bug2_ioctl_example_2.bpl(1577,3): inline$I8xDeviceControl$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(1590,3): inline$I8xDeviceControl$0$label_13_true#2
daytona_bug2_ioctl_example_2.bpl(1598,3): inline$I8xDeviceControl$0$label_14_false#2
daytona_bug2_ioctl_example_2.bpl(1627,3): inline$IoGetCurrentIrpStackLocation$2$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1631,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2
daytona_bug2_ioctl_example_2.bpl(1644,3): inline$I8xDeviceControl$0$anon16_Else#2
daytona_bug2_ioctl_example_2.bpl(1657,3): inline$I8xDeviceControl$0$label_19_case_2#2
daytona_bug2_ioctl_example_2.bpl(1721,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1725,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2
daytona_bug2_ioctl_example_2.bpl(1738,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2
daytona_bug2_ioctl_example_2.bpl(1751,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2
daytona_bug2_ioctl_example_2.bpl(1759,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2
daytona_bug2_ioctl_example_2.bpl(1813,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2
daytona_bug2_ioctl_example_2.bpl(1837,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2
daytona_bug2_ioctl_example_2.bpl(1845,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2
daytona_bug2_ioctl_example_2.bpl(1869,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2
daytona_bug2_ioctl_example_2.bpl(1874,3): inline$storm_KeAcquireSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(1885,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1890,3): inline$storm_KeAcquireSpinLock$0$anon9#2
daytona_bug2_ioctl_example_2.bpl(1894,3): inline$storm_KeAcquireSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(1911,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
daytona_bug2_ioctl_example_2.bpl(1922,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
daytona_bug2_ioctl_example_2.bpl(1953,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2
daytona_bug2_ioctl_example_2.bpl(2012,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2
daytona_bug2_ioctl_example_2.bpl(2016,3): inline$storm_IoSetCancelRoutine$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(2036,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(2041,3): inline$storm_IoSetCancelRoutine$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(2052,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2057,3): inline$storm_IoSetCancelRoutine$0$anon10#2
daytona_bug2_ioctl_example_2.bpl(2064,3): inline$storm_IoSetCancelRoutine$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2077,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
daytona_bug2_ioctl_example_2.bpl(2202,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
daytona_bug2_ioctl_example_2.bpl(2210,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2
daytona_bug2_ioctl_example_2.bpl(2220,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2
daytona_bug2_ioctl_example_2.bpl(2248,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2
daytona_bug2_ioctl_example_2.bpl(2295,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2
daytona_bug2_ioctl_example_2.bpl(2303,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2
daytona_bug2_ioctl_example_2.bpl(2313,3): inline$storm_IoSetCancelRoutine$1$anon5#2
daytona_bug2_ioctl_example_2.bpl(2321,3): inline$storm_IoSetCancelRoutine$1$anon14_Else#2
daytona_bug2_ioctl_example_2.bpl(2329,3): inline$storm_IoSetCancelRoutine$1$anon15_Then#2
daytona_bug2_ioctl_example_2.bpl(2339,3): inline$storm_IoSetCancelRoutine$1$anon8#2
daytona_bug2_ioctl_example_2.bpl(2350,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2355,3): inline$storm_IoSetCancelRoutine$1$anon10#2
daytona_bug2_ioctl_example_2.bpl(2363,3): inline$storm_IoSetCancelRoutine$1$label_1#2
daytona_bug2_ioctl_example_2.bpl(2377,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
daytona_bug2_ioctl_example_2.bpl(2387,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
daytona_bug2_ioctl_example_2.bpl(2409,3): inline$storm_IoMarkIrpPending$2$label_6_false#2
daytona_bug2_ioctl_example_2.bpl(2449,3): inline$storm_IoMarkIrpPending$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2462,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2
daytona_bug2_ioctl_example_2.bpl(2509,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2
daytona_bug2_ioctl_example_2.bpl(2535,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2
daytona_bug2_ioctl_example_2.bpl(2576,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(2583,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2
daytona_bug2_ioctl_example_2.bpl(2591,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2
daytona_bug2_ioctl_example_2.bpl(2601,3): inline$storm_KeReleaseSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(2612,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(2617,3): inline$storm_KeReleaseSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(2621,3): inline$storm_KeReleaseSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2634,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
daytona_bug2_ioctl_example_2.bpl(2867,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2
daytona_bug2_ioctl_example_2.bpl(2910,3): inline$storm_IoCompleteRequest$2$label_6_false#2
daytona_bug2_ioctl_example_2.bpl(2953,3): inline$storm_IoCompleteRequest$2$anon6_Else#2
daytona_bug2_ioctl_example_2.bpl(2961,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
daytona_bug2_ioctl_example_2.bpl(2971,3): inline$storm_IoCompleteRequest$2$anon2#2
daytona_bug2_ioctl_example_2.bpl(2975,3): inline$storm_IoCompleteRequest$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2988,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
daytona_bug2_ioctl_example_2.bpl(3008,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
daytona_bug2_ioctl_example_2.bpl(3015,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2
daytona_bug2_ioctl_example_2.bpl(3159,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3177,3): inline$I8xDeviceControl$0$anon18_Else#2
daytona_bug2_ioctl_example_2.bpl(3646,3): inline$I8xDeviceControl$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3663,3): inline$dispatch$0$anon5_Else#2
daytona_bug2_ioctl_example_2.bpl(3694,3): anon31_Then#2
daytona_bug2_ioctl_example_2.bpl(3699,3): anon17#2
daytona_bug2_ioctl_example_2.bpl(3756,3): inline$storm_IoCancelIrp$0$anon23_Then#2
daytona_bug2_ioctl_example_2.bpl(3761,3): inline$storm_IoCancelIrp$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(3785,3): inline$storm_IoCancelIrp$0$anon25_Then#2
daytona_bug2_ioctl_example_2.bpl(3790,3): inline$storm_IoCancelIrp$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3811,3): inline$storm_IoCancelIrp$0$anon27_Then#2
daytona_bug2_ioctl_example_2.bpl(3816,3): inline$storm_IoCancelIrp$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(3827,3): inline$storm_IoCancelIrp$0$anon29_Then#2
daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2
daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(3953,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3966,3): inline$storm_IoCancelIrp$0$anon30_Else#2
daytona_bug2_ioctl_example_2.bpl(3984,3): inline$storm_IoCancelIrp$0$label_16_true#2
daytona_bug2_ioctl_example_2.bpl(4002,3): inline$storm_IoCancelIrp$0$label_22_true#2
daytona_bug2_ioctl_example_2.bpl(4010,3): inline$storm_IoCancelIrp$0$anon32_Else#2
daytona_bug2_ioctl_example_2.bpl(4023,3): inline$storm_IoCancelIrp$0$label_27_false#2
daytona_bug2_ioctl_example_2.bpl(4724,3): inline$storm_IoCancelIrp$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(4759,3): inline$cancel$0$anon2_Then#2
daytona_bug2_ioctl_example_2.bpl(4773,3): anon32_Then#2
daytona_bug2_ioctl_example_2.bpl(4778,3): anon19#2
daytona_bug2_ioctl_example_2.bpl(4816,3): anon33_Then#2
daytona_bug2_ioctl_example_2.bpl(4821,3): anon21#2
Boogie program verifier finished with 0 verified, 1 error
|
