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
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
|
bla1.bpl(2095,5): Error BP5001: This assertion might not hold.
Execution trace:
bla1.bpl(749,3): start#1
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(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(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
bla1.bpl(986,3): inline$IoGetNextIrpStackLocation$0$anon2#1
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(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
bla1.bpl(1117,3): inline$IoSetNextIrpStackLocation$0$anon5#1
bla1.bpl(1157,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#1
bla1.bpl(1162,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1
bla1.bpl(1197,3): anon12_Then#1
bla1.bpl(1202,3): anon5#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
bla1.bpl(1312,3): inline$I8xDeviceControl$0$anon2#1
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(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
bla1.bpl(1438,3): inline$storm_IoSetCancelRoutine$0$anon11_Else#1
bla1.bpl(1446,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#1
bla1.bpl(1456,3): inline$storm_IoSetCancelRoutine$0$anon6#1
bla1.bpl(1467,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1
bla1.bpl(1472,3): inline$storm_IoSetCancelRoutine$0$anon8#1
bla1.bpl(1524,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1
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(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
bla1.bpl(1651,3): inline$storm_IoCompleteRequest$0$label_7#1
bla1.bpl(1654,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1
bla1.bpl(1676,3): inline$storm_IoCompleteRequest$0$label_1#1
bla1.bpl(1734,3): anon14_Then#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
bla1.bpl(1820,3): inline$storm_IoCancelIrp$0$anon15_Then#1
bla1.bpl(1830,3): inline$storm_IoCancelIrp$0$anon5#1
bla1.bpl(1838,3): inline$storm_IoCancelIrp$0$anon16_Else#1
bla1.bpl(1846,3): inline$storm_IoCancelIrp$0$anon17_Then#1
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(1932,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#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
bla1.bpl(1976,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1
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(2036,3): inline$storm_IoCancelIrp$0$label_25_false#1
bla1.bpl(2054,3): inline$storm_IoCancelIrp$0$label_1#1
bla1.bpl(2076,3): anon15_Then#1
bla1.bpl(2081,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(4833,5): Error BP5001: This assertion might not hold.
Execution trace:
daytona_bug2_ioctl_example_2.bpl(805,3): start#2
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(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
daytona_bug2_ioctl_example_2.bpl(941,3): inline$storm_IoAllocateIrp$0$anon5#2
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(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
daytona_bug2_ioctl_example_2.bpl(1051,3): inline$IoGetNextIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1066,3): inline$storm_IoAllocateIrp$0$anon27_Else#2
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(1129,3): anon24_Else#2
daytona_bug2_ioctl_example_2.bpl(1144,3): anon25_Else#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
daytona_bug2_ioctl_example_2.bpl(1212,3): inline$IoSetNextIrpStackLocation$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(1225,3): anon26_Else#2
daytona_bug2_ioctl_example_2.bpl(1259,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1264,3): inline$IoGetCurrentIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1279,3): anon27_Else#2
daytona_bug2_ioctl_example_2.bpl(1306,3): anon28_Then#2
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(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(1422,3): anon30_Else#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
daytona_bug2_ioctl_example_2.bpl(1534,3): inline$I8xDeviceControl$0$anon13_Else#2
daytona_bug2_ioctl_example_2.bpl(1557,3): inline$I8xDeviceControl$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1562,3): inline$I8xDeviceControl$0$anon4#2
daytona_bug2_ioctl_example_2.bpl(1575,3): inline$I8xDeviceControl$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(1588,3): inline$I8xDeviceControl$0$label_13_true#2
daytona_bug2_ioctl_example_2.bpl(1596,3): inline$I8xDeviceControl$0$label_14_false#2
daytona_bug2_ioctl_example_2.bpl(1625,3): inline$IoGetCurrentIrpStackLocation$2$anon3_Then#2
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(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(1811,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#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(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(1892,3): inline$storm_KeAcquireSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#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(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
daytona_bug2_ioctl_example_2.bpl(2039,3): inline$storm_IoSetCancelRoutine$0$anon8#2
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(2062,3): inline$storm_IoSetCancelRoutine$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#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(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
daytona_bug2_ioctl_example_2.bpl(2319,3): inline$storm_IoSetCancelRoutine$1$anon14_Else#2
daytona_bug2_ioctl_example_2.bpl(2327,3): inline$storm_IoSetCancelRoutine$1$anon15_Then#2
daytona_bug2_ioctl_example_2.bpl(2337,3): inline$storm_IoSetCancelRoutine$1$anon8#2
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(2361,3): inline$storm_IoSetCancelRoutine$1$label_1#2
daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#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(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(2533,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#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
daytona_bug2_ioctl_example_2.bpl(2599,3): inline$storm_KeReleaseSpinLock$0$anon5#2
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(2619,3): inline$storm_KeReleaseSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#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
daytona_bug2_ioctl_example_2.bpl(2908,3): inline$storm_IoCompleteRequest$2$label_6_false#2
daytona_bug2_ioctl_example_2.bpl(2948,3): inline$storm_IoCompleteRequest$2$label_7#2
daytona_bug2_ioctl_example_2.bpl(2951,3): inline$storm_IoCompleteRequest$2$anon6_Else#2
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(2973,3): inline$storm_IoCompleteRequest$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#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(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
daytona_bug2_ioctl_example_2.bpl(3013,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#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(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(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(3692,3): anon31_Then#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
daytona_bug2_ioctl_example_2.bpl(3788,3): inline$storm_IoCancelIrp$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3809,3): inline$storm_IoCancelIrp$0$anon27_Then#2
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(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(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(3951,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#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(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(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(4776,3): anon19#2
daytona_bug2_ioctl_example_2.bpl(4814,3): anon33_Then#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(1197,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
stack_overflow.bpl(1230,3): inline$storm_IoAllocateIrp$0$anon6_Else#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(1364,3): anon10_Else#1
stack_overflow.bpl(1379,3): anon11_Else#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(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(1569,3): inline$myInitDriver$0$anon8_Else#1
stack_overflow.bpl(1605,3): inline$myInitDriver$0$anon9_Else#1
stack_overflow.bpl(1641,3): inline$myInitDriver$0$anon10_Else#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(1710,3): anon14_Else#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(1877,3): inline$BDLPnP$0$anon54_Else#1
stack_overflow.bpl(1891,3): inline$BDLPnP$0$label_16_true#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(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(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(77742,3): inline$BDLPnPStart$0$anon36_Else#1
stack_overflow.bpl(77756,3): inline$BDLPnPStart$0$label_11_true#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(77858,3): inline$BDLPnPStart$0$anon38_Else#1
stack_overflow.bpl(77872,3): inline$BDLPnPStart$0$label_31_true#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(78066,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#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(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
stack_overflow.bpl(78233,3): inline$storm_IoSetCompletionRoutine$0$label_1#1
stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#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
stack_overflow.bpl(83279,3): inline$BDLCallLowerLevelDriverAndWait$0$label_18_true#1
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(83403,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(83409,3): inline$IoSetNextIrpStackLocation$2$label_5#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(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(87162,3): inline$CallCompletionRoutine$3$label_20_icall_2#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(87365,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1
stack_overflow.bpl(87379,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#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
stack_overflow.bpl(87483,3): inline$BDLDevicePowerIoCompletion$3$label_44_true#1
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(87613,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1
stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#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(87692,3): inline$BDLDevicePowerIoCompletion$3$label_83#1
stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
stack_overflow.bpl(87702,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1
stack_overflow.bpl(87713,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1
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(87782,3): inline$storm_IoCompleteRequest$7$label_1#1
stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#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(87895,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1
stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#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(87974,3): inline$BDLDevicePowerIoCompletion$3$label_122#1
stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#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(88160,3): inline$CallCompletionRoutine$3$label_24_true#1
stack_overflow.bpl(88169,3): inline$CallCompletionRoutine$3$label_1#1
stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#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(88222,3): inline$storm_IoCallDriver$1$label_1#1
stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#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(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(88477,3): inline$BDLCallLowerLevelDriverAndWait$0$Return#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(89073,3): inline$BDLPnPStart$0$anon42_Else#1
stack_overflow.bpl(89087,3): inline$BDLPnPStart$0$label_66_true#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(89234,3): inline$BDLPnPStart$0$anon45_Else#1
stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#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(89313,3): inline$BDLPnPStart$0$label_102#1
stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#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(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(94710,3): inline$BDLPnP$0$anon75_Then#1
stack_overflow.bpl(95206,3): inline$BDLPnP$0$Return#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(95294,3): inline$storm_IoCancelIrp$0$anon9_Then#1
stack_overflow.bpl(95299,3): inline$storm_IoCancelIrp$0$anon1#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(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(97935,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
|
