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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
|
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
Boogie program verifier finished with 1 verified, 0 errors
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
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
Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
|
