1extern char __VERIFIER_nondet_char(void);
2extern int __VERIFIER_nondet_int(void);
3extern long __VERIFIER_nondet_long(void);
4extern void *__VERIFIER_nondet_pointer(void);
5void errorFn(void) ;
6void IofCompleteRequest(int Irp , int PriorityBoost );
7extern int __VERIFIER_nondet_int();
8int KernelMode ;
9int Executive ;
10int DevicePowerState ;
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 52
33 s = NP;
34#line 53
35 pended = 0;
36#line 54
37 compFptr = 0;
38#line 55
39 compRegistered = 0;
40#line 56
41 lowerDriverReturn = 0;
42#line 57
43 setEventCalled = 0;
44#line 58
45 customIrp = 0;
46#line 59
47 return;
48}
49}
50#line 62 "kbfiltr_simpl2.cil.c"
51void _BLAST_init(void)
52{
53
54 {
55#line 66
56 UNLOADED = 0;
57#line 67
58 NP = 1;
59#line 68
60 DC = 2;
61#line 69
62 SKIP1 = 3;
63#line 70
64 SKIP2 = 4;
65#line 71
66 MPR1 = 5;
67#line 72
68 MPR3 = 6;
69#line 73
70 IPC = 7;
71#line 74
72 s = UNLOADED;
73#line 75
74 pended = 0;
75#line 76
76 compFptr = 0;
77#line 77
78 compRegistered = 0;
79#line 78
80 lowerDriverReturn = 0;
81#line 79
82 setEventCalled = 0;
83#line 80
84 customIrp = 0;
85#line 81
86 return;
87}
88}
89#line 84 "kbfiltr_simpl2.cil.c"
90int KbFilter_PnP(int DeviceObject , int Irp )
91{ int devExt ;
92 int irpStack ;
93 int status ;
94 int event = __VERIFIER_nondet_int() ;
95 int DeviceObject__DeviceExtension = __VERIFIER_nondet_int() ;
96 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
97 int irpStack__MinorFunction = __VERIFIER_nondet_int() ;
98 int devExt__TopOfStack = __VERIFIER_nondet_int() ;
99 int devExt__Started ;
100 int devExt__Removed ;
101 int devExt__SurpriseRemoved ;
102 int Irp__IoStatus__Status ;
103 int Irp__IoStatus__Information ;
104 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
105 int irpSp ;
106 int nextIrpSp ;
107 int nextIrpSp__Control ;
108 int irpSp___0 ;
109 int irpSp__Context ;
110 int irpSp__Control ;
111 long __cil_tmp23 ;
112
113 {
114#line 107
115 status = 0;
116#line 108
117 devExt = DeviceObject__DeviceExtension;
118#line 109
119 irpStack = Irp__Tail__Overlay__CurrentStackLocation;
120#line 110
121 if (irpStack__MinorFunction == 0) {
122 goto switch_0_0;
123 } else {
124#line 113
125 if (irpStack__MinorFunction == 23) {
126 goto switch_0_23;
127 } else {
128#line 116
129 if (irpStack__MinorFunction == 2) {
130 goto switch_0_2;
131 } else {
132#line 119
133 if (irpStack__MinorFunction == 1) {
134 goto switch_0_1;
135 } else {
136#line 122
137 if (irpStack__MinorFunction == 5) {
138 goto switch_0_1;
139 } else {
140#line 125
141 if (irpStack__MinorFunction == 3) {
142 goto switch_0_1;
143 } else {
144#line 128
145 if (irpStack__MinorFunction == 6) {
146 goto switch_0_1;
147 } else {
148#line 131
149 if (irpStack__MinorFunction == 13) {
150 goto switch_0_1;
151 } else {
152#line 134
153 if (irpStack__MinorFunction == 4) {
154 goto switch_0_1;
155 } else {
156#line 137
157 if (irpStack__MinorFunction == 7) {
158 goto switch_0_1;
159 } else {
160#line 140
161 if (irpStack__MinorFunction == 8) {
162 goto switch_0_1;
163 } else {
164#line 143
165 if (irpStack__MinorFunction == 9) {
166 goto switch_0_1;
167 } else {
168#line 146
169 if (irpStack__MinorFunction == 12) {
170 goto switch_0_1;
171 } else {
172#line 149
173 if (irpStack__MinorFunction == 10) {
174 goto switch_0_1;
175 } else {
176#line 152
177 if (irpStack__MinorFunction == 11) {
178 goto switch_0_1;
179 } else {
180#line 155
181 if (irpStack__MinorFunction == 15) {
182 goto switch_0_1;
183 } else {
184#line 158
185 if (irpStack__MinorFunction == 16) {
186 goto switch_0_1;
187 } else {
188#line 161
189 if (irpStack__MinorFunction == 17) {
190 goto switch_0_1;
191 } else {
192#line 164
193 if (irpStack__MinorFunction == 18) {
194 goto switch_0_1;
195 } else {
196#line 167
197 if (irpStack__MinorFunction == 19) {
198 goto switch_0_1;
199 } else {
200#line 170
201 if (irpStack__MinorFunction == 20) {
202 goto switch_0_1;
203 } else {
204 goto switch_0_1;
205#line 175
206 if (0) {
207 switch_0_0:
208#line 177
209 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
210#line 178
211 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
212#line 179
213 nextIrpSp__Control = 0;
214#line 180
215 if (s != NP) {
216 {
217#line 182
218 errorFn();
219 }
220 } else {
221#line 185
222 if (compRegistered != 0) {
223 {
224#line 187
225 errorFn();
226 }
227 } else {
228#line 190
229 compRegistered = 1;
230 }
231 }
232 {
233#line 194
234 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation - 1;
235#line 195
236 irpSp__Context = event;
237#line 196
238 irpSp__Control = 224;
239#line 200
240 status = IofCallDriver(devExt__TopOfStack,
241 Irp);
242 }
243 {
244#line 203
245 __cil_tmp23 = (long )status;
246#line 203
247 if (__cil_tmp23 == 259) {
248 {
249#line 205
250 KeWaitForSingleObject(event, Executive,
251 KernelMode,
252 0, 0);
253 }
254 }
255 }
256#line 212
257 if (status >= 0) {
258#line 213
259 if (myStatus >= 0) {
260#line 214
261 devExt__Started = 1;
262#line 215
263 devExt__Removed = 0;
264#line 216
265 devExt__SurpriseRemoved = 0;
266 }
267 }
268 {
269#line 224
270 Irp__IoStatus__Status = status;
271#line 225
272 myStatus = status;
273#line 226
274 Irp__IoStatus__Information = 0;
275#line 227
276 IofCompleteRequest(Irp, 0);
277 }
278 goto switch_0_break;
279 switch_0_23:
280#line 231
281 devExt__SurpriseRemoved = 1;
282#line 232
283 if (s == NP) {
284#line 233
285 s = SKIP1;
286 } else {
287 {
288#line 236
289 errorFn();
290 }
291 }
292 {
293#line 240
294 Irp__CurrentLocation ++;
295#line 241
296 Irp__Tail__Overlay__CurrentStackLocation ++;
297#line 242
298 status = IofCallDriver(devExt__TopOfStack,
299 Irp);
300 }
301 goto switch_0_break;
302 switch_0_2:
303#line 247
304 devExt__Removed = 1;
305#line 248
306 if (s == NP) {
307#line 249
308 s = SKIP1;
309 } else {
310 {
311#line 252
312 errorFn();
313 }
314 }
315 {
316#line 256
317 Irp__CurrentLocation ++;
318#line 257
319 Irp__Tail__Overlay__CurrentStackLocation ++;
320#line 258
321 IofCallDriver(devExt__TopOfStack, Irp);
322#line 259
323 status = 0;
324 }
325 goto switch_0_break;
326 switch_0_1: ;
327#line 281
328 if (s == NP) {
329#line 282
330 s = SKIP1;
331 } else {
332 {
333#line 285
334 errorFn();
335 }
336 }
337 {
338#line 289
339 Irp__CurrentLocation ++;
340#line 290
341 Irp__Tail__Overlay__CurrentStackLocation ++;
342#line 291
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 320
372 return (status);
373}
374}
375#line 323 "kbfiltr_simpl2.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 KernelMode = 0;
386 Executive = 0;
387 DevicePowerState = 1;
388 s = 0;
389 UNLOADED = 0;
390 NP = 0;
391 DC = 0;
392 SKIP1 = 0;
393 SKIP2 = 0 ;
394 MPR1 = 0;
395 MPR3 = 0;
396 IPC = 0;
397 pended = 0;
398 compFptr = 0;
399 compRegistered = 0;
400 lowerDriverReturn = 0;
401 setEventCalled = 0;
402 customIrp = 0;
403 myStatus = 0;
404
405 {
406 {
407#line 334
408 status = 0;
409#line 335
410 pirp = irp;
411#line 336
412 _BLAST_init();
413 }
414#line 338
415 if (status >= 0) {
416#line 339
417 s = NP;
418#line 340
419 customIrp = 0;
420#line 341
421 setEventCalled = customIrp;
422#line 342
423 lowerDriverReturn = setEventCalled;
424#line 343
425 compRegistered = lowerDriverReturn;
426#line 344
427 pended = compRegistered;
428#line 345
429 pirp__IoStatus__Status = 0;
430#line 346
431 myStatus = 0;
432#line 347
433 if (irp_choice == 0) {
434#line 348
435 pirp__IoStatus__Status = -1073741637;
436#line 349
437 myStatus = -1073741637;
438 }
439 {
440#line 354
441 stub_driver_init();
442 }
443 {
444#line 356
445#line 356
446 if (status < 0) {
447#line 357
448 return (-1);
449 }
450 }
451#line 361
452 int tmp_ndt_1;
453 tmp_ndt_1 = __VERIFIER_nondet_int();
454 if (tmp_ndt_1 == 0) {
455 goto switch_1_0;
456 } else {
457#line 364
458 int tmp_ndt_2;
459 tmp_ndt_2 = __VERIFIER_nondet_int();
460 if (tmp_ndt_2 == 1) {
461 goto switch_1_1;
462 } else {
463#line 367
464 int tmp_ndt_3;
465 tmp_ndt_3 = __VERIFIER_nondet_int();
466 if (tmp_ndt_3 == 3) {
467 goto switch_1_3;
468 } else {
469#line 370
470 int tmp_ndt_4;
471 tmp_ndt_4 = __VERIFIER_nondet_int();
472 if (tmp_ndt_4 == 4) {
473 goto switch_1_4;
474 } else {
475#line 373
476 int tmp_ndt_5;
477 tmp_ndt_5 = __VERIFIER_nondet_int();
478 if (tmp_ndt_5 == 8) {
479 goto switch_1_8;
480 } else {
481 goto switch_1_default;
482#line 378
483 if (0) {
484 switch_1_0:
485 {
486#line 381
487 status = KbFilter_CreateClose(devobj, pirp);
488 }
489 goto switch_1_break;
490 switch_1_1:
491 {
492#line 386
493 status = KbFilter_CreateClose(devobj, pirp);
494 }
495 goto switch_1_break;
496 switch_1_3:
497 {
498#line 391
499 status = KbFilter_PnP(devobj, pirp);
500 }
501 goto switch_1_break;
502 switch_1_4:
503 {
504#line 396
505 status = KbFilter_Power(devobj, pirp);
506 }
507 goto switch_1_break;
508 switch_1_8:
509 {
510#line 401
511 status = KbFilter_InternIoCtl(devobj, pirp);
512 }
513 goto switch_1_break;
514 switch_1_default: ;
515#line 405
516 return (-1);
517 } else {
518 switch_1_break: ;
519 }
520 }
521 }
522 }
523 }
524 }
525 }
526#line 418
527 if (pended == 1) {
528#line 419
529 if (s == NP) {
530#line 420
531 s = NP;
532 } else {
533 goto _L___2;
534 }
535 } else {
536 _L___2:
537#line 426
538 if (pended == 1) {
539#line 427
540 if (s == MPR3) {
541#line 428
542 s = MPR3;
543 } else {
544 goto _L___1;
545 }
546 } else {
547 _L___1:
548#line 434
549 if (s != UNLOADED) {
550#line 437
551 if (status != -1) {
552#line 440
553 if (s != SKIP2) {
554#line 441
555 if (s != IPC) {
556#line 442
557 if (s == DC) {
558 goto _L___0;
559 }
560 } else {
561 goto _L___0;
562 }
563 } else {
564 _L___0:
565#line 452
566 if (pended == 1) {
567#line 453
568 if (status != 259) {
569 {
570#line 455
571 errorFn();
572 }
573 }
574 } else {
575#line 461
576 if (s == DC) {
577#line 462
578 if (status == 259) {
579
580 }
581 } else {
582#line 468
583 if (status != lowerDriverReturn) {
584 errorFn();
585 }
586 else{
587 }
588 }
589 }
590 }
591 }
592 }
593 }
594 }
595#line 480
596 return (status);
597}
598}
599#line 483 "kbfiltr_simpl2.cil.c"
600void stubMoreProcessingRequired(void)
601{
602
603 {
604#line 487
605 if (s == NP) {
606#line 488
607 s = MPR1;
608 } else {
609 {
610#line 491
611 errorFn();
612 }
613 }
614#line 494
615 return;
616}
617}
618#line 497 "kbfiltr_simpl2.cil.c"
619int IofCallDriver(int DeviceObject , int Irp )
620{
621 int returnVal2 ;
622 int compRetStatus ;
623 int lcontext = __VERIFIER_nondet_int() ;
624 long long __cil_tmp7 ;
625
626 {
627#line 504
628 if (compRegistered) {
629 {
630#line 506
631 compRetStatus = KbFilter_Complete(DeviceObject, Irp, lcontext);
632 }
633 {
634#line 508
635 __cil_tmp7 = (long long )compRetStatus;
636#line 508
637 if (__cil_tmp7 == -1073741802) {
638 {
639#line 510
640 stubMoreProcessingRequired();
641 }
642 }
643 }
644 }
645#line 518
646 int tmp_ndt_6;
647 tmp_ndt_6 = __VERIFIER_nondet_int();
648 if (tmp_ndt_6 == 0) {
649 goto switch_2_0;
650 } else {
651#line 521
652 int tmp_ndt_7;
653 tmp_ndt_7 = __VERIFIER_nondet_int();
654 if (tmp_ndt_7 == 1) {
655 goto switch_2_1;
656 } else {
657 goto switch_2_default;
658#line 526
659 if (0) {
660 switch_2_0:
661#line 528
662 returnVal2 = 0;
663 goto switch_2_break;
664 switch_2_1:
665#line 531
666 returnVal2 = -1073741823;
667 goto switch_2_break;
668 switch_2_default:
669#line 534
670 returnVal2 = 259;
671 goto switch_2_break;
672 } else {
673 switch_2_break: ;
674 }
675 }
676 }
677#line 542
678 if (s == NP) {
679#line 543
680 s = IPC;
681#line 544
682 lowerDriverReturn = returnVal2;
683 } else {
684#line 546
685 if (s == MPR1) {
686#line 547
687 if (returnVal2 == 259) {
688#line 548
689 s = MPR3;
690#line 549
691 lowerDriverReturn = returnVal2;
692 } else {
693#line 551
694 s = NP;
695#line 552
696 lowerDriverReturn = returnVal2;
697 }
698 } else {
699#line 555
700 if (s == SKIP1) {
701#line 556
702 s = SKIP2;
703#line 557
704 lowerDriverReturn = returnVal2;
705 } else {
706 {
707#line 560
708 errorFn();
709 }
710 }
711 }
712 }
713#line 565
714 return (returnVal2);
715}
716}
717#line 568 "kbfiltr_simpl2.cil.c"
718void IofCompleteRequest(int Irp , int PriorityBoost )
719{
720
721 {
722#line 572
723 if (s == NP) {
724#line 573
725 s = DC;
726 } else {
727 {
728#line 576
729 errorFn();
730 }
731 }
732#line 579
733 return;
734}
735}
736#line 582 "kbfiltr_simpl2.cil.c"
737int KeSetEvent(int Event , int Increment , int Wait )
738{ int l = __VERIFIER_nondet_int() ;
739
740 {
741#line 586
742 setEventCalled = 1;
743#line 587
744 return (l);
745}
746}
747#line 590 "kbfiltr_simpl2.cil.c"
748int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
749 int Timeout )
750{
751
752 {
753#line 595
754 if (s == MPR3) {
755#line 596
756 if (setEventCalled == 1) {
757#line 597
758 s = NP;
759#line 598
760 setEventCalled = 0;
761 } else {
762 goto _L;
763 }
764 } else {
765 _L:
766#line 604
767 if (customIrp == 1) {
768#line 605
769 s = NP;
770#line 606
771 customIrp = 0;
772 } else {
773#line 608
774 if (s == MPR3) {
775 {
776#line 610
777 errorFn();
778 }
779 }
780 }
781 }
782#line 617
783 int tmp_ndt_8;
784 tmp_ndt_8 = __VERIFIER_nondet_int();
785 if (tmp_ndt_8 == 0) {
786 goto switch_3_0;
787 } else {
788 goto switch_3_default;
789#line 622
790 if (0) {
791 switch_3_0:
792#line 624
793 return (0);
794 switch_3_default: ;
795#line 626
796 return (-1073741823);
797 } else {
798
799 }
800 }
801}
802}
803#line 634 "kbfiltr_simpl2.cil.c"
804int KbFilter_Complete(int DeviceObject , int Irp , int Context )
805{ int event ;
806
807 {
808 {
809#line 639
810 event = Context;
811#line 640
812 KeSetEvent(event, 0, 0);
813 }
814#line 642
815 return (-1073741802);
816}
817}
818#line 645 "kbfiltr_simpl2.cil.c"
819int KbFilter_CreateClose(int DeviceObject , int Irp )
820{ int irpStack__MajorFunction = __VERIFIER_nondet_int() ;
821 int devExt__UpperConnectData__ClassService = __VERIFIER_nondet_int() ;
822 int Irp__IoStatus__Status ;
823 int status ;
824 int tmp ;
825
826 {
827#line 653
828 status = myStatus;
829#line 654
830 if (irpStack__MajorFunction == 0) {
831 goto switch_4_0;
832 } else {
833#line 657
834 if (irpStack__MajorFunction == 2) {
835 goto switch_4_2;
836 } else {
837#line 660
838 if (0) {
839 switch_4_0: ;
840#line 662
841 if (devExt__UpperConnectData__ClassService == 0) {
842#line 663
843 status = -1073741436;
844 }
845 goto switch_4_break;
846 switch_4_2: ;
847 goto switch_4_break;
848 } else {
849 switch_4_break: ;
850 }
851 }
852 }
853 {
854#line 676
855 Irp__IoStatus__Status = status;
856#line 677
857 myStatus = status;
858#line 678
859 tmp = KbFilter_DispatchPassThrough(DeviceObject, Irp);
860 }
861#line 680
862 return (tmp);
863}
864}
865#line 683 "kbfiltr_simpl2.cil.c"
866int KbFilter_DispatchPassThrough(int DeviceObject , int Irp )
867{ int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
868 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
869 int DeviceObject__DeviceExtension__TopOfStack = __VERIFIER_nondet_int() ;
870 int irpStack ;
871 int tmp ;
872
873 {
874#line 691
875 irpStack = Irp__Tail__Overlay__CurrentStackLocation;
876#line 692
877 if (s == NP) {
878#line 693
879 s = SKIP1;
880 } else {
881 {
882#line 696
883 errorFn();
884 }
885 }
886 {
887#line 700
888 Irp__CurrentLocation ++;
889#line 701
890 Irp__Tail__Overlay__CurrentStackLocation ++;
891#line 702
892 tmp = IofCallDriver(DeviceObject__DeviceExtension__TopOfStack, Irp);
893 }
894#line 704
895 return (tmp);
896}
897}
898#line 707 "kbfiltr_simpl2.cil.c"
899int KbFilter_Power(int DeviceObject , int Irp )
900{ int irpStack__MinorFunction = __VERIFIER_nondet_int() ;
901 int devExt__DeviceState ;
902 int powerState__DeviceState = __VERIFIER_nondet_int() ;
903 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
904 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
905 int devExt__TopOfStack = __VERIFIER_nondet_int() ;
906 int powerType = __VERIFIER_nondet_int() ;
907 int tmp ;
908
909 {
910#line 718
911 if (irpStack__MinorFunction == 2) {
912 goto switch_5_2;
913 } else {
914#line 721
915 if (irpStack__MinorFunction == 1) {
916 goto switch_5_1;
917 } else {
918#line 724
919 if (irpStack__MinorFunction == 0) {
920 goto switch_5_0;
921 } else {
922#line 727
923 if (irpStack__MinorFunction == 3) {
924 goto switch_5_3;
925 } else {
926 goto switch_5_default;
927#line 732
928 if (0) {
929 switch_5_2: ;
930#line 734
931 if (powerType == DevicePowerState) {
932#line 735
933 devExt__DeviceState = powerState__DeviceState;
934 }
935 switch_5_1: ;
936 switch_5_0: ;
937 switch_5_3: ;
938 switch_5_default: ;
939 goto switch_5_break;
940 } else {
941 switch_5_break: ;
942 }
943 }
944 }
945 }
946 }
947#line 752
948 if (s == NP) {
949#line 753
950 s = SKIP1;
951 } else {
952 {
953#line 756
954 errorFn();
955 }
956 }
957 {
958#line 760
959 Irp__CurrentLocation ++;
960#line 761
961 Irp__Tail__Overlay__CurrentStackLocation ++;
962#line 762
963 tmp = PoCallDriver(devExt__TopOfStack, Irp);
964 }
965#line 764
966 return (tmp);
967}
968}
969#line 767 "kbfiltr_simpl2.cil.c"
970int PoCallDriver(int DeviceObject , int Irp )
971{
972 int compRetStatus ;
973 int returnVal ;
974 int lcontext = __VERIFIER_nondet_int() ;
975 unsigned long __cil_tmp7 ;
976 long __cil_tmp8 ;
977
978 {
979#line 774
980 if (compRegistered) {
981 {
982#line 776
983 compRetStatus = KbFilter_Complete(DeviceObject, Irp, lcontext);
984 }
985 {
986#line 778
987 __cil_tmp7 = (unsigned long )compRetStatus;
988#line 778
989 if (__cil_tmp7 == -1073741802) {
990 {
991#line 780
992 stubMoreProcessingRequired();
993 }
994 }
995 }
996 }
997#line 788
998 int tmp_ndt_9;
999 tmp_ndt_9 = __VERIFIER_nondet_int();
1000 if (tmp_ndt_9 == 0) {
1001 goto switch_6_0;
1002 } else {
1003#line 791
1004 int tmp_ndt_10;
1005 tmp_ndt_10 = __VERIFIER_nondet_int();
1006 if (tmp_ndt_10 == 1) {
1007 goto switch_6_1;
1008 } else {
1009 goto switch_6_default;
1010#line 796
1011 if (0) {
1012 switch_6_0:
1013#line 798
1014 returnVal = 0;
1015 goto switch_6_break;
1016 switch_6_1:
1017#line 801
1018 returnVal = -1073741823;
1019 goto switch_6_break;
1020 switch_6_default:
1021#line 804
1022 returnVal = 259;
1023 goto switch_6_break;
1024 } else {
1025 switch_6_break: ;
1026 }
1027 }
1028 }
1029#line 812
1030 if (s == NP) {
1031#line 813
1032 s = IPC;
1033#line 814
1034 lowerDriverReturn = returnVal;
1035 } else {
1036#line 816
1037 if (s == MPR1) {
1038 {
1039#line 817
1040 __cil_tmp8 = (long )returnVal;
1041#line 817
1042 if (__cil_tmp8 == 259L) {
1043#line 818
1044 s = MPR3;
1045#line 819
1046 lowerDriverReturn = returnVal;
1047 } else {
1048#line 821
1049 s = NP;
1050#line 822
1051 lowerDriverReturn = returnVal;
1052 }
1053 }
1054 } else {
1055#line 825
1056 if (s == SKIP1) {
1057#line 826
1058 s = SKIP2;
1059#line 827
1060 lowerDriverReturn = returnVal;
1061 } else {
1062 {
1063#line 830
1064 errorFn();
1065 }
1066 }
1067 }
1068 }
1069#line 835
1070 return (returnVal);
1071}
1072}
1073#line 838 "kbfiltr_simpl2.cil.c"
1074int KbFilter_InternIoCtl(int DeviceObject , int Irp )
1075{ int Irp__IoStatus__Information ;
1076 int irpStack__Parameters__DeviceIoControl__IoControlCode = __VERIFIER_nondet_int() ;
1077 int devExt__UpperConnectData__ClassService = __VERIFIER_nondet_int() ;
1078 int irpStack__Parameters__DeviceIoControl__InputBufferLength = __VERIFIER_nondet_int() ;
1079 int sizeof__CONNECT_DATA = __VERIFIER_nondet_int() ;
1080 int irpStack__Parameters__DeviceIoControl__Type3InputBuffer = __VERIFIER_nondet_int() ;
1081 int sizeof__INTERNAL_I8042_HOOK_KEYBOARD = __VERIFIER_nondet_int() ;
1082 int hookKeyboard__InitializationRoutine = __VERIFIER_nondet_int() ;
1083 int hookKeyboard__IsrRoutine = __VERIFIER_nondet_int() ;
1084 int Irp__IoStatus__Status ;
1085 int hookKeyboard ;
1086 int connectData ;
1087 int status ;
1088 int tmp ;
1089 int __cil_tmp17 ;
1090 int __cil_tmp18 ;
1091 int __cil_tmp19 ;
1092 int __cil_tmp20 = __VERIFIER_nondet_int() ;
1093 int __cil_tmp21 ;
1094 int __cil_tmp22 ;
1095 int __cil_tmp23 ;
1096 int __cil_tmp24 = __VERIFIER_nondet_int() ;
1097 int __cil_tmp25 ;
1098 int __cil_tmp26 ;
1099 int __cil_tmp27 ;
1100 int __cil_tmp28 = __VERIFIER_nondet_int() ;
1101 int __cil_tmp29 = __VERIFIER_nondet_int() ;
1102 int __cil_tmp30 ;
1103 int __cil_tmp31 ;
1104 int __cil_tmp32 = __VERIFIER_nondet_int() ;
1105 int __cil_tmp33 ;
1106 int __cil_tmp34 ;
1107 int __cil_tmp35 = __VERIFIER_nondet_int() ;
1108 int __cil_tmp36 ;
1109 int __cil_tmp37 ;
1110 int __cil_tmp38 = __VERIFIER_nondet_int() ;
1111 int __cil_tmp39 ;
1112 int __cil_tmp40 ;
1113 int __cil_tmp41 = __VERIFIER_nondet_int() ;
1114 int __cil_tmp42 ;
1115 int __cil_tmp43 ;
1116 int __cil_tmp44 = __VERIFIER_nondet_int() ;
1117 int __cil_tmp45 ;
1118
1119 {
1120#line 855
1121 status = 0;
1122#line 856
1123 Irp__IoStatus__Information = 0;
1124 {
1125#line 857
1126
1127#line 857
1128
1129#line 857
1130
1131#line 857
1132
1133#line 857
1134 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp20) {
1135 goto switch_7_exp_0;
1136 } else {
1137 {
1138#line 860
1139
1140#line 860
1141
1142#line 860
1143
1144#line 860
1145
1146#line 860
1147 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp24) {
1148 goto switch_7_exp_1;
1149 } else {
1150 {
1151#line 863
1152
1153#line 863
1154
1155#line 863
1156
1157#line 863
1158
1159#line 863
1160 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp28) {
1161 goto switch_7_exp_2;
1162 } else {
1163 {
1164#line 866
1165
1166#line 866
1167 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp29) {
1168 goto switch_7_exp_3;
1169 } else {
1170 {
1171#line 869
1172
1173#line 869
1174
1175#line 869
1176
1177#line 869
1178 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp32) {
1179 goto switch_7_exp_4;
1180 } else {
1181 {
1182#line 872
1183
1184#line 872
1185
1186#line 872
1187
1188#line 872
1189 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp35) {
1190 goto switch_7_exp_5;
1191 } else {
1192 {
1193#line 875
1194
1195#line 875
1196
1197#line 875
1198
1199#line 875
1200 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp38) {
1201 goto switch_7_exp_6;
1202 } else {
1203 {
1204#line 878
1205
1206#line 878
1207
1208#line 878
1209
1210#line 878
1211 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp41) {
1212 goto switch_7_exp_7;
1213 } else {
1214 {
1215#line 881
1216
1217#line 881
1218
1219#line 881
1220
1221#line 881
1222 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp44) {
1223 goto switch_7_exp_8;
1224 } else {
1225#line 884
1226 if (0) {
1227 switch_7_exp_0: ;
1228#line 886
1229 if (devExt__UpperConnectData__ClassService != 0) {
1230#line 887
1231 status = -1073741757;
1232 goto switch_7_break;
1233 } else {
1234#line 890
1235 if (irpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CONNECT_DATA) {
1236#line 891
1237 status = -1073741811;
1238 goto switch_7_break;
1239 }
1240 }
1241#line 897
1242 connectData = irpStack__Parameters__DeviceIoControl__Type3InputBuffer;
1243 goto switch_7_break;
1244 switch_7_exp_1:
1245#line 900
1246 status = -1073741822;
1247 goto switch_7_break;
1248 switch_7_exp_2: ;
1249#line 903
1250 if (irpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__INTERNAL_I8042_HOOK_KEYBOARD) {
1251#line 904
1252 status = -1073741811;
1253 goto switch_7_break;
1254 }
1255#line 909
1256 hookKeyboard = irpStack__Parameters__DeviceIoControl__Type3InputBuffer;
1257#line 910
1258 if (hookKeyboard__InitializationRoutine) {
1259
1260 }
1261#line 915
1262 if (hookKeyboard__IsrRoutine) {
1263
1264 }
1265#line 920
1266 status = 0;
1267 goto switch_7_break;
1268 switch_7_exp_3: ;
1269 switch_7_exp_4: ;
1270 switch_7_exp_5: ;
1271 switch_7_exp_6: ;
1272 switch_7_exp_7: ;
1273 switch_7_exp_8: ;
1274 goto switch_7_break;
1275 } else {
1276 switch_7_break: ;
1277 }
1278 }
1279 }
1280 }
1281 }
1282 }
1283 }
1284 }
1285 }
1286 }
1287 }
1288 }
1289 }
1290 }
1291 }
1292 }
1293 }
1294 }
1295 }
1296 {
1297#line 941
1298#line 941
1299 if (status < 0) {
1300 {
1301#line 943
1302 Irp__IoStatus__Status = status;
1303#line 944
1304 myStatus = status;
1305#line 945
1306 IofCompleteRequest(Irp, 0);
1307 }
1308#line 947
1309 return (status);
1310 }
1311 }
1312 {
1313#line 952
1314 tmp = KbFilter_DispatchPassThrough(DeviceObject, Irp);
1315 }
1316#line 954
1317 return (tmp);
1318}
1319}
1320
1321void errorFn(void)
1322{
1323
1324 {
1325 goto ERROR;
1326 ERROR:
1327#line 29
1328 return;
1329}
1330}