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