1
2
3
4int KernelMode ;
5int Executive ;
6int s ;
7int UNLOADED ;
8int NP ;
9int DC ;
10int SKIP1 ;
11int SKIP2 ;
12int MPR1 ;
13int MPR3 ;
14int IPC ;
15int pended ;
16int compFptr ;
17int compRegistered ;
18int lowerDriverReturn ;
19int setEventCalled ;
20int customIrp ;
21int myStatus ;
22
23void stub_driver_init(void)
24{
25
26 {
27#line 46
28 s = NP;
29#line 47
30 pended = 0;
31#line 48
32 compFptr = 0;
33#line 49
34 compRegistered = 0;
35#line 50
36 lowerDriverReturn = 0;
37#line 51
38 setEventCalled = 0;
39#line 52
40 customIrp = 0;
41#line 53
42 return;
43}
44}
45#line 56 "kbfiltr_simpl1.cil.c"
46void _BLAST_init(void)
47{
48
49 {
50#line 60
51 UNLOADED = 0;
52#line 61
53 NP = 1;
54#line 62
55 DC = 2;
56#line 63
57 SKIP1 = 3;
58#line 64
59 SKIP2 = 4;
60#line 65
61 MPR1 = 5;
62#line 66
63 MPR3 = 6;
64#line 67
65 IPC = 7;
66#line 68
67 s = UNLOADED;
68#line 69
69 pended = 0;
70#line 70
71 compFptr = 0;
72#line 71
73 compRegistered = 0;
74#line 72
75 lowerDriverReturn = 0;
76#line 73
77 setEventCalled = 0;
78#line 74
79 customIrp = 0;
80#line 75
81 return;
82}
83}
84#line 78 "kbfiltr_simpl1.cil.c"
85void IofCompleteRequest(int, int);
86void errorFn(void);
87int KbFilter_PnP(int DeviceObject , int Irp )
88{ int devExt ;
89 int irpStack ;
90 int status ;
91 int event ;
92 int DeviceObject__DeviceExtension ;
93 int Irp__Tail__Overlay__CurrentStackLocation ;
94 int irpStack__MinorFunction ;
95 int devExt__TopOfStack ;
96 int devExt__Started ;
97 int devExt__Removed ;
98 int devExt__SurpriseRemoved ;
99 int Irp__IoStatus__Status ;
100 int Irp__IoStatus__Information ;
101 int Irp__CurrentLocation ;
102 int irpSp ;
103 int nextIrpSp ;
104 int nextIrpSp__Control ;
105 int irpSp___0 ;
106 int irpSp__Context ;
107 int irpSp__Control ;
108 long __cil_tmp23 ;
109
110 {
111#line 101
112 status = 0;
113#line 102
114 devExt = DeviceObject__DeviceExtension;
115#line 103
116 irpStack = Irp__Tail__Overlay__CurrentStackLocation;
117#line 104
118 if (irpStack__MinorFunction == 0) {
119 goto switch_0_0;
120 } else {
121#line 107
122 if (irpStack__MinorFunction == 23) {
123 goto switch_0_23;
124 } else {
125#line 110
126 if (irpStack__MinorFunction == 2) {
127 goto switch_0_2;
128 } else {
129#line 113
130 if (irpStack__MinorFunction == 1) {
131 goto switch_0_1;
132 } else {
133#line 116
134 if (irpStack__MinorFunction == 5) {
135 goto switch_0_1;
136 } else {
137#line 119
138 if (irpStack__MinorFunction == 3) {
139 goto switch_0_1;
140 } else {
141#line 122
142 if (irpStack__MinorFunction == 6) {
143 goto switch_0_1;
144 } else {
145#line 125
146 if (irpStack__MinorFunction == 13) {
147 goto switch_0_1;
148 } else {
149#line 128
150 if (irpStack__MinorFunction == 4) {
151 goto switch_0_1;
152 } else {
153#line 131
154 if (irpStack__MinorFunction == 7) {
155 goto switch_0_1;
156 } else {
157#line 134
158 if (irpStack__MinorFunction == 8) {
159 goto switch_0_1;
160 } else {
161#line 137
162 if (irpStack__MinorFunction == 9) {
163 goto switch_0_1;
164 } else {
165#line 140
166 if (irpStack__MinorFunction == 12) {
167 goto switch_0_1;
168 } else {
169#line 143
170 if (irpStack__MinorFunction == 10) {
171 goto switch_0_1;
172 } else {
173#line 146
174 if (irpStack__MinorFunction == 11) {
175 goto switch_0_1;
176 } else {
177#line 149
178 if (irpStack__MinorFunction == 15) {
179 goto switch_0_1;
180 } else {
181#line 152
182 if (irpStack__MinorFunction == 16) {
183 goto switch_0_1;
184 } else {
185#line 155
186 if (irpStack__MinorFunction == 17) {
187 goto switch_0_1;
188 } else {
189#line 158
190 if (irpStack__MinorFunction == 18) {
191 goto switch_0_1;
192 } else {
193#line 161
194 if (irpStack__MinorFunction == 19) {
195 goto switch_0_1;
196 } else {
197#line 164
198 if (irpStack__MinorFunction == 20) {
199 goto switch_0_1;
200 } else {
201 goto switch_0_1;
202#line 169
203 if (0) {
204 switch_0_0:
205#line 171
206 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
207#line 172
208 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
209#line 173
210 nextIrpSp__Control = 0;
211#line 174
212 if (s != NP) {
213 {
214#line 176
215 errorFn();
216 }
217 } else {
218#line 179
219 if (compRegistered != 0) {
220 {
221#line 181
222 errorFn();
223 }
224 } else {
225#line 184
226 compRegistered = 1;
227 }
228 }
229 {
230#line 188
231 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation - 1;
232#line 189
233 irpSp__Control = 224;
234#line 192
235 status = IofCallDriver(devExt__TopOfStack,
236 Irp);
237 }
238 {
239#line 197
240 __cil_tmp23 = (long )status;
241#line 197
242 if (__cil_tmp23 == 259 ) {
243 {
244#line 199
245 KeWaitForSingleObject(event, Executive,
246 KernelMode,
247 0, 0);
248 }
249 }
250 }
251#line 206
252 if (status >= 0) {
253#line 207
254 if (myStatus >= 0) {
255#line 208
256 devExt__Started = 1;
257#line 209
258 devExt__Removed = 0;
259#line 210
260 devExt__SurpriseRemoved = 0;
261 }
262 }
263 {
264#line 218
265 Irp__IoStatus__Status = status;
266#line 219
267 myStatus = status;
268#line 220
269 Irp__IoStatus__Information = 0;
270#line 221
271 IofCompleteRequest(Irp, 0);
272 }
273 goto switch_0_break;
274 switch_0_23:
275#line 225
276 devExt__SurpriseRemoved = 1;
277#line 226
278 if (s == NP) {
279#line 227
280 s = SKIP1;
281 } else {
282 {
283#line 230
284 errorFn();
285 }
286 }
287 {
288#line 234
289 Irp__CurrentLocation ++;
290#line 235
291 Irp__Tail__Overlay__CurrentStackLocation ++;
292#line 236
293 status = IofCallDriver(devExt__TopOfStack,
294 Irp);
295 }
296 goto switch_0_break;
297 switch_0_2:
298#line 241
299 devExt__Removed = 1;
300#line 242
301 if (s == NP) {
302#line 243
303 s = SKIP1;
304 } else {
305 {
306#line 246
307 errorFn();
308 }
309 }
310 {
311#line 250
312 Irp__CurrentLocation ++;
313#line 251
314 Irp__Tail__Overlay__CurrentStackLocation ++;
315#line 252
316 IofCallDriver(devExt__TopOfStack, Irp);
317#line 253
318 status = 0;
319 }
320 goto switch_0_break;
321 switch_0_1: ;
322#line 275
323 if (s == NP) {
324#line 276
325 s = SKIP1;
326 } else {
327 {
328#line 279
329 errorFn();
330 }
331 }
332 {
333#line 283
334 Irp__CurrentLocation ++;
335#line 284
336 Irp__Tail__Overlay__CurrentStackLocation ++;
337#line 285
338 status = IofCallDriver(devExt__TopOfStack,
339 Irp);
340 }
341 goto switch_0_break;
342 } else {
343 switch_0_break: ;
344 }
345 }
346 }
347 }
348 }
349 }
350 }
351 }
352 }
353 }
354 }
355 }
356 }
357 }
358 }
359 }
360 }
361 }
362 }
363 }
364 }
365 }
366#line 314
367 return (status);
368}
369}
370#line 317 "kbfiltr_simpl1.cil.c"
371int main(void)
372{ int status ;
373 int irp ;
374 int pirp ;
375 int pirp__IoStatus__Status ;
376
377 int irp_choice ;
378 int devobj ;
379 int __cil_tmp8 ;
380
381 {
382 {
383;
384KernelMode = 0 ;
385 Executive = 0;
386s = 0;
387UNLOADED = 0;
388NP = 0;
389 DC = 0;
390 SKIP1 = 0;
391 SKIP2 = 0;
392 MPR1 = 0;
393 MPR3 = 0;
394 IPC = 0;
395 pended = 0;
396 compFptr = 0;
397 compRegistered = 0;
398 lowerDriverReturn = 0;
399 setEventCalled = 0;
400 customIrp = 0;
401 myStatus = 0;
402
403#line 328
404 status = 0;
405#line 329
406 pirp = irp;
407#line 330
408 _BLAST_init();
409 }
410#line 332
411 if (status >= 0) {
412#line 333
413 s = NP;
414#line 334
415 customIrp = 0;
416#line 335
417 setEventCalled = customIrp;
418#line 336
419 lowerDriverReturn = setEventCalled;
420#line 337
421 compRegistered = lowerDriverReturn;
422#line 338
423 pended = compRegistered;
424#line 339
425 pirp__IoStatus__Status = 0;
426#line 340
427 myStatus = 0;
428#line 341
429 if (irp_choice == 0) {
430#line 342
431 pirp__IoStatus__Status = -1073741637;
432#line 343
433 myStatus = -1073741637;
434 }
435 {
436#line 348
437 stub_driver_init();
438 }
439 {
440#line 350
441 if(status >= 0){
442 __cil_tmp8 = 1;
443 }
444 else{
445 __cil_tmp8 = 0;
446 }
447#line 350
448 if (! __cil_tmp8) {
449#line 351
450 return (-1);
451 }
452 }
453#line 355
454 int tmp_ndt_1;
455 tmp_ndt_1 = __VERIFIER_nondet_int();
456 if (tmp_ndt_1 == 3) {
457 goto switch_1_3;
458 } else {
459 goto switch_1_default;
460#line 360
461 if (0) {
462 switch_1_3:
463 {
464#line 363
465 status = KbFilter_PnP(devobj, pirp);
466 }
467 goto switch_1_break;
468 switch_1_default: ;
469#line 367
470 return (-1);
471 } else {
472 switch_1_break: ;
473 }
474 }
475 }
476#line 376
477 if (pended == 1) {
478#line 377
479 if (s == NP) {
480#line 378
481 s = NP;
482 } else {
483 goto _L___2;
484 }
485 } else {
486 _L___2:
487#line 384
488 if (pended == 1) {
489#line 385
490 if (s == MPR3) {
491#line 386
492 s = MPR3;
493 } else {
494 goto _L___1;
495 }
496 } else {
497 _L___1:
498#line 392
499 if (s != UNLOADED) {
500#line 395
501 if (status != -1) {
502#line 398
503 if (s != SKIP2) {
504#line 399
505 if (s != IPC) {
506#line 400
507 if (s == DC) {
508 goto _L___0;
509 }
510 } else {
511 goto _L___0;
512 }
513 } else {
514 _L___0:
515#line 410
516 if (pended == 1) {
517#line 411
518 if (status != 259) {
519 {
520#line 413
521 errorFn();
522 }
523 }
524 } else {
525#line 419
526 if (s == DC) {
527#line 420
528 if (status == 259) {
529
530 }
531 } else {
532#line 426
533 if (status != lowerDriverReturn) {
534
535 }
536 }
537 }
538 }
539 }
540 }
541 }
542 }
543
544 return (status);
545}
546}
547#line 441 "kbfiltr_simpl1.cil.c"
548void stubMoreProcessingRequired(void)
549{
550
551 {
552#line 445
553 if (s == NP) {
554#line 446
555 s = MPR1;
556 } else {
557 {
558#line 449
559 errorFn();
560 }
561 }
562#line 452
563 return;
564}
565}
566#line 455 "kbfiltr_simpl1.cil.c"
567int IofCallDriver(int DeviceObject , int Irp )
568{
569 int returnVal2 ;
570 int compRetStatus ;
571 int lcontext ;
572 long long __cil_tmp7 ;
573;
574 {
575#line 462
576 if (compRegistered) {
577 compRetStatus = KbFilter_Complete(DeviceObject, Irp, lcontext);
578 stubMoreProcessingRequired();
579 }
580#line 476
581 int tmp_ndt_2;
582 tmp_ndt_2 = __VERIFIER_nondet_int();
583 if (tmp_ndt_2 == 0) {
584 goto switch_2_0;
585 } else {
586#line 479
587 int tmp_ndt_3;
588 tmp_ndt_3 = __VERIFIER_nondet_int();
589 if (tmp_ndt_3 == 1) {
590 goto switch_2_1;
591 } else {
592 goto switch_2_default;
593#line 484
594 if (0) {
595 switch_2_0:
596#line 486
597 returnVal2 = 0;
598 goto switch_2_break;
599 switch_2_1:
600#line 489
601 returnVal2 = -1073741823;
602 goto switch_2_break;
603 switch_2_default:
604#line 492
605 returnVal2 = 259;
606 goto switch_2_break;
607 } else {
608 switch_2_break: ;
609 }
610 }
611 }
612#line 500
613 if (s == NP) {
614#line 501
615 s = IPC;
616#line 502
617 lowerDriverReturn = returnVal2;
618 } else {
619#line 504
620 if (s == MPR1) {
621#line 505
622 if (returnVal2 == 259) {
623#line 506
624 s = MPR3;
625#line 507
626 lowerDriverReturn = returnVal2;
627 } else {
628#line 509
629 s = NP;
630#line 510
631 lowerDriverReturn = returnVal2;
632 }
633 } else {
634#line 513
635 if (s == SKIP1) {
636#line 514
637 s = SKIP2;
638#line 515
639 lowerDriverReturn = returnVal2;
640 } else {
641 {
642#line 518
643 errorFn();
644 }
645 }
646 }
647 }
648#line 523
649 return (returnVal2);
650}
651}
652#line 526 "kbfiltr_simpl1.cil.c"
653void IofCompleteRequest(int Irp , int PriorityBoost )
654{
655
656 {
657#line 530
658 if (s == NP) {
659#line 531
660 s = DC;
661 } else {
662 {
663#line 534
664 errorFn();
665 }
666 }
667#line 537
668 return;
669}
670}
671#line 540 "kbfiltr_simpl1.cil.c"
672int KeSetEvent(int Event , int Increment , int Wait )
673{ int l ;
674
675 {
676#line 544
677 setEventCalled = 1;
678#line 545
679 return (l);
680}
681}
682#line 548 "kbfiltr_simpl1.cil.c"
683int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
684 int Timeout )
685{
686;
687 {
688#line 553
689 if (s == MPR3) {
690#line 554
691 if (setEventCalled == 1) {
692#line 555
693 s = NP;
694#line 556
695 setEventCalled = 0;
696 } else {
697 goto _L;
698 }
699 } else {
700 _L:
701#line 562
702 if (customIrp == 1) {
703#line 563
704 s = NP;
705#line 564
706 customIrp = 0;
707 } else {
708#line 566
709 if (s == MPR3) {
710 {
711#line 568
712 errorFn();
713 }
714 }
715 }
716 }
717#line 575
718 int tmp_ndt_4;
719 tmp_ndt_4 = __VERIFIER_nondet_int();
720 if (tmp_ndt_4 == 0) {
721 goto switch_3_0;
722 } else {
723 goto switch_3_default;
724#line 580
725 if (0) {
726 switch_3_0:
727#line 582
728 return (0);
729 switch_3_default: ;
730#line 584
731 return (-1073741823);
732 } else {
733
734 }
735 }
736}
737}
738#line 592 "kbfiltr_simpl1.cil.c"
739int KbFilter_Complete(int DeviceObject , int Irp , int Context )
740{ int event ;
741
742 {
743 {
744#line 597
745 event = Context;
746#line 598
747 KeSetEvent(event, 0, 0);
748 }
749#line 600
750 return (-1073741802);
751}
752}
753
754void errorFn(void)
755{
756
757 {
758 goto ERROR;
759 ERROR:
760#line 23
761 return;
762}
763}