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();
6int KernelMode ;
7int Executive ;
8int DevicePowerState ;
9int s ;
10int UNLOADED ;
11int NP ;
12int DC ;
13int SKIP1 ;
14int SKIP2 ;
15int MPR1 ;
16int MPR3 ;
17int IPC ;
18int pended ;
19int compFptr ;
20int compRegistered ;
21int lowerDriverReturn ;
22int setEventCalled ;
23int customIrp ;
24int myStatus ;
25
26void stub_driver_init(void)
27{
28
29 {
30#line 52
31 s = NP;
32#line 53
33 pended = 0;
34#line 54
35 compFptr = 0;
36#line 55
37 compRegistered = 0;
38#line 56
39 lowerDriverReturn = 0;
40#line 57
41 setEventCalled = 0;
42#line 58
43 customIrp = 0;
44#line 59
45 return;
46}
47}
48#line 62 "kbfiltr_simpl2.cil.c"
49void _BLAST_init(void)
50{
51
52 {
53#line 66
54 UNLOADED = 0;
55#line 67
56 NP = 1;
57#line 68
58 DC = 2;
59#line 69
60 SKIP1 = 3;
61#line 70
62 SKIP2 = 4;
63#line 71
64 MPR1 = 5;
65#line 72
66 MPR3 = 6;
67#line 73
68 IPC = 7;
69#line 74
70 s = UNLOADED;
71#line 75
72 pended = 0;
73#line 76
74 compFptr = 0;
75#line 77
76 compRegistered = 0;
77#line 78
78 lowerDriverReturn = 0;
79#line 79
80 setEventCalled = 0;
81#line 80
82 customIrp = 0;
83#line 81
84 return;
85}
86}
87#line 84 "kbfiltr_simpl2.cil.c"
88void IofCompleteRequest(int, int);
89void errorFn(void);
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
585 }
586 }
587 }
588 }
589 }
590 }
591 }
592 }
593#line 480
594 return (status);
595}
596}
597#line 483 "kbfiltr_simpl2.cil.c"
598void stubMoreProcessingRequired(void)
599{
600
601 {
602#line 487
603 if (s == NP) {
604#line 488
605 s = MPR1;
606 } else {
607 {
608#line 491
609 errorFn();
610 }
611 }
612#line 494
613 return;
614}
615}
616#line 497 "kbfiltr_simpl2.cil.c"
617int IofCallDriver(int DeviceObject , int Irp )
618{
619 int returnVal2 ;
620 int compRetStatus ;
621 int lcontext = __VERIFIER_nondet_int() ;
622 long long __cil_tmp7 ;
623
624 {
625#line 504
626 if (compRegistered) {
627 {
628#line 506
629 compRetStatus = KbFilter_Complete(DeviceObject, Irp, lcontext);
630 }
631 {
632#line 508
633 __cil_tmp7 = (long long )compRetStatus;
634#line 508
635 if (__cil_tmp7 == -1073741802) {
636 {
637#line 510
638 stubMoreProcessingRequired();
639 }
640 }
641 }
642 }
643#line 518
644 int tmp_ndt_6;
645 tmp_ndt_6 = __VERIFIER_nondet_int();
646 if (tmp_ndt_6 == 0) {
647 goto switch_2_0;
648 } else {
649#line 521
650 int tmp_ndt_7;
651 tmp_ndt_7 = __VERIFIER_nondet_int();
652 if (tmp_ndt_7 == 1) {
653 goto switch_2_1;
654 } else {
655 goto switch_2_default;
656#line 526
657 if (0) {
658 switch_2_0:
659#line 528
660 returnVal2 = 0;
661 goto switch_2_break;
662 switch_2_1:
663#line 531
664 returnVal2 = -1073741823;
665 goto switch_2_break;
666 switch_2_default:
667#line 534
668 returnVal2 = 259;
669 goto switch_2_break;
670 } else {
671 switch_2_break: ;
672 }
673 }
674 }
675#line 542
676 if (s == NP) {
677#line 543
678 s = IPC;
679#line 544
680 lowerDriverReturn = returnVal2;
681 } else {
682#line 546
683 if (s == MPR1) {
684#line 547
685 if (returnVal2 == 259) {
686#line 548
687 s = MPR3;
688#line 549
689 lowerDriverReturn = returnVal2;
690 } else {
691#line 551
692 s = NP;
693#line 552
694 lowerDriverReturn = returnVal2;
695 }
696 } else {
697#line 555
698 if (s == SKIP1) {
699#line 556
700 s = SKIP2;
701#line 557
702 lowerDriverReturn = returnVal2;
703 } else {
704 {
705#line 560
706 errorFn();
707 }
708 }
709 }
710 }
711#line 565
712 return (returnVal2);
713}
714}
715#line 568 "kbfiltr_simpl2.cil.c"
716void IofCompleteRequest(int Irp , int PriorityBoost )
717{
718
719 {
720#line 572
721 if (s == NP) {
722#line 573
723 s = DC;
724 } else {
725 {
726#line 576
727 errorFn();
728 }
729 }
730#line 579
731 return;
732}
733}
734#line 582 "kbfiltr_simpl2.cil.c"
735int KeSetEvent(int Event , int Increment , int Wait )
736{ int l = __VERIFIER_nondet_int() ;
737
738 {
739#line 586
740 setEventCalled = 1;
741#line 587
742 return (l);
743}
744}
745#line 590 "kbfiltr_simpl2.cil.c"
746int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
747 int Timeout )
748{
749
750 {
751#line 595
752 if (s == MPR3) {
753#line 596
754 if (setEventCalled == 1) {
755#line 597
756 s = NP;
757#line 598
758 setEventCalled = 0;
759 } else {
760 goto _L;
761 }
762 } else {
763 _L:
764#line 604
765 if (customIrp == 1) {
766#line 605
767 s = NP;
768#line 606
769 customIrp = 0;
770 } else {
771#line 608
772 if (s == MPR3) {
773 {
774#line 610
775 errorFn();
776 }
777 }
778 }
779 }
780#line 617
781 int tmp_ndt_8;
782 tmp_ndt_8 = __VERIFIER_nondet_int();
783 if (tmp_ndt_8 == 0) {
784 goto switch_3_0;
785 } else {
786 goto switch_3_default;
787#line 622
788 if (0) {
789 switch_3_0:
790#line 624
791 return (0);
792 switch_3_default: ;
793#line 626
794 return (-1073741823);
795 } else {
796
797 }
798 }
799}
800}
801#line 634 "kbfiltr_simpl2.cil.c"
802int KbFilter_Complete(int DeviceObject , int Irp , int Context )
803{ int event ;
804
805 {
806 {
807#line 639
808 event = Context;
809#line 640
810 KeSetEvent(event, 0, 0);
811 }
812#line 642
813 return (-1073741802);
814}
815}
816#line 645 "kbfiltr_simpl2.cil.c"
817int KbFilter_CreateClose(int DeviceObject , int Irp )
818{ int irpStack__MajorFunction = __VERIFIER_nondet_int() ;
819 int devExt__UpperConnectData__ClassService = __VERIFIER_nondet_int() ;
820 int Irp__IoStatus__Status ;
821 int status ;
822 int tmp ;
823
824 {
825#line 653
826 status = myStatus;
827#line 654
828 if (irpStack__MajorFunction == 0) {
829 goto switch_4_0;
830 } else {
831#line 657
832 if (irpStack__MajorFunction == 2) {
833 goto switch_4_2;
834 } else {
835#line 660
836 if (0) {
837 switch_4_0: ;
838#line 662
839 if (devExt__UpperConnectData__ClassService == 0) {
840#line 663
841 status = -1073741436;
842 }
843 goto switch_4_break;
844 switch_4_2: ;
845 goto switch_4_break;
846 } else {
847 switch_4_break: ;
848 }
849 }
850 }
851 {
852#line 676
853 Irp__IoStatus__Status = status;
854#line 677
855 myStatus = status;
856#line 678
857 tmp = KbFilter_DispatchPassThrough(DeviceObject, Irp);
858 }
859#line 680
860 return (tmp);
861}
862}
863#line 683 "kbfiltr_simpl2.cil.c"
864int KbFilter_DispatchPassThrough(int DeviceObject , int Irp )
865{ int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
866 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
867 int DeviceObject__DeviceExtension__TopOfStack = __VERIFIER_nondet_int() ;
868 int irpStack ;
869 int tmp ;
870
871 {
872#line 691
873 irpStack = Irp__Tail__Overlay__CurrentStackLocation;
874#line 692
875 if (s == NP) {
876#line 693
877 s = SKIP1;
878 } else {
879 {
880#line 696
881 errorFn();
882 }
883 }
884 {
885#line 700
886 Irp__CurrentLocation ++;
887#line 701
888 Irp__Tail__Overlay__CurrentStackLocation ++;
889#line 702
890 tmp = IofCallDriver(DeviceObject__DeviceExtension__TopOfStack, Irp);
891 }
892#line 704
893 return (tmp);
894}
895}
896#line 707 "kbfiltr_simpl2.cil.c"
897int KbFilter_Power(int DeviceObject , int Irp )
898{ int irpStack__MinorFunction = __VERIFIER_nondet_int() ;
899 int devExt__DeviceState ;
900 int powerState__DeviceState = __VERIFIER_nondet_int() ;
901 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
902 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
903 int devExt__TopOfStack = __VERIFIER_nondet_int() ;
904 int powerType = __VERIFIER_nondet_int() ;
905 int tmp ;
906
907 {
908#line 718
909 if (irpStack__MinorFunction == 2) {
910 goto switch_5_2;
911 } else {
912#line 721
913 if (irpStack__MinorFunction == 1) {
914 goto switch_5_1;
915 } else {
916#line 724
917 if (irpStack__MinorFunction == 0) {
918 goto switch_5_0;
919 } else {
920#line 727
921 if (irpStack__MinorFunction == 3) {
922 goto switch_5_3;
923 } else {
924 goto switch_5_default;
925#line 732
926 if (0) {
927 switch_5_2: ;
928#line 734
929 if (powerType == DevicePowerState) {
930#line 735
931 devExt__DeviceState = powerState__DeviceState;
932 }
933 switch_5_1: ;
934 switch_5_0: ;
935 switch_5_3: ;
936 switch_5_default: ;
937 goto switch_5_break;
938 } else {
939 switch_5_break: ;
940 }
941 }
942 }
943 }
944 }
945#line 752
946 if (s == NP) {
947#line 753
948 s = SKIP1;
949 } else {
950 {
951#line 756
952 errorFn();
953 }
954 }
955 {
956#line 760
957 Irp__CurrentLocation ++;
958#line 761
959 Irp__Tail__Overlay__CurrentStackLocation ++;
960#line 762
961 tmp = PoCallDriver(devExt__TopOfStack, Irp);
962 }
963#line 764
964 return (tmp);
965}
966}
967#line 767 "kbfiltr_simpl2.cil.c"
968int PoCallDriver(int DeviceObject , int Irp )
969{
970 int compRetStatus ;
971 int returnVal ;
972 int lcontext = __VERIFIER_nondet_int() ;
973 unsigned long __cil_tmp7 ;
974 long __cil_tmp8 ;
975
976 {
977#line 774
978 if (compRegistered) {
979 {
980#line 776
981 compRetStatus = KbFilter_Complete(DeviceObject, Irp, lcontext);
982 }
983 {
984#line 778
985 __cil_tmp7 = (unsigned long )compRetStatus;
986#line 778
987 if (__cil_tmp7 == -1073741802) {
988 {
989#line 780
990 stubMoreProcessingRequired();
991 }
992 }
993 }
994 }
995#line 788
996 int tmp_ndt_9;
997 tmp_ndt_9 = __VERIFIER_nondet_int();
998 if (tmp_ndt_9 == 0) {
999 goto switch_6_0;
1000 } else {
1001#line 791
1002 int tmp_ndt_10;
1003 tmp_ndt_10 = __VERIFIER_nondet_int();
1004 if (tmp_ndt_10 == 1) {
1005 goto switch_6_1;
1006 } else {
1007 goto switch_6_default;
1008#line 796
1009 if (0) {
1010 switch_6_0:
1011#line 798
1012 returnVal = 0;
1013 goto switch_6_break;
1014 switch_6_1:
1015#line 801
1016 returnVal = -1073741823;
1017 goto switch_6_break;
1018 switch_6_default:
1019#line 804
1020 returnVal = 259;
1021 goto switch_6_break;
1022 } else {
1023 switch_6_break: ;
1024 }
1025 }
1026 }
1027#line 812
1028 if (s == NP) {
1029#line 813
1030 s = IPC;
1031#line 814
1032 lowerDriverReturn = returnVal;
1033 } else {
1034#line 816
1035 if (s == MPR1) {
1036 {
1037#line 817
1038 __cil_tmp8 = (long )returnVal;
1039#line 817
1040 if (__cil_tmp8 == 259L) {
1041#line 818
1042 s = MPR3;
1043#line 819
1044 lowerDriverReturn = returnVal;
1045 } else {
1046#line 821
1047 s = NP;
1048#line 822
1049 lowerDriverReturn = returnVal;
1050 }
1051 }
1052 } else {
1053#line 825
1054 if (s == SKIP1) {
1055#line 826
1056 s = SKIP2;
1057#line 827
1058 lowerDriverReturn = returnVal;
1059 } else {
1060 {
1061#line 830
1062 errorFn();
1063 }
1064 }
1065 }
1066 }
1067#line 835
1068 return (returnVal);
1069}
1070}
1071#line 838 "kbfiltr_simpl2.cil.c"
1072int KbFilter_InternIoCtl(int DeviceObject , int Irp )
1073{ int Irp__IoStatus__Information ;
1074 int irpStack__Parameters__DeviceIoControl__IoControlCode = __VERIFIER_nondet_int() ;
1075 int devExt__UpperConnectData__ClassService = __VERIFIER_nondet_int() ;
1076 int irpStack__Parameters__DeviceIoControl__InputBufferLength = __VERIFIER_nondet_int() ;
1077 int sizeof__CONNECT_DATA = __VERIFIER_nondet_int() ;
1078 int irpStack__Parameters__DeviceIoControl__Type3InputBuffer = __VERIFIER_nondet_int() ;
1079 int sizeof__INTERNAL_I8042_HOOK_KEYBOARD = __VERIFIER_nondet_int() ;
1080 int hookKeyboard__InitializationRoutine = __VERIFIER_nondet_int() ;
1081 int hookKeyboard__IsrRoutine = __VERIFIER_nondet_int() ;
1082 int Irp__IoStatus__Status ;
1083 int hookKeyboard ;
1084 int connectData ;
1085 int status ;
1086 int tmp ;
1087 int __cil_tmp17 ;
1088 int __cil_tmp18 ;
1089 int __cil_tmp19 ;
1090 int __cil_tmp20 = __VERIFIER_nondet_int() ;
1091 int __cil_tmp21 ;
1092 int __cil_tmp22 ;
1093 int __cil_tmp23 ;
1094 int __cil_tmp24 = __VERIFIER_nondet_int() ;
1095 int __cil_tmp25 ;
1096 int __cil_tmp26 ;
1097 int __cil_tmp27 ;
1098 int __cil_tmp28 = __VERIFIER_nondet_int() ;
1099 int __cil_tmp29 = __VERIFIER_nondet_int() ;
1100 int __cil_tmp30 ;
1101 int __cil_tmp31 ;
1102 int __cil_tmp32 = __VERIFIER_nondet_int() ;
1103 int __cil_tmp33 ;
1104 int __cil_tmp34 ;
1105 int __cil_tmp35 = __VERIFIER_nondet_int() ;
1106 int __cil_tmp36 ;
1107 int __cil_tmp37 ;
1108 int __cil_tmp38 = __VERIFIER_nondet_int() ;
1109 int __cil_tmp39 ;
1110 int __cil_tmp40 ;
1111 int __cil_tmp41 = __VERIFIER_nondet_int() ;
1112 int __cil_tmp42 ;
1113 int __cil_tmp43 ;
1114 int __cil_tmp44 = __VERIFIER_nondet_int() ;
1115 int __cil_tmp45 ;
1116
1117 {
1118#line 855
1119 status = 0;
1120#line 856
1121 Irp__IoStatus__Information = 0;
1122 {
1123#line 857
1124
1125#line 857
1126
1127#line 857
1128
1129#line 857
1130
1131#line 857
1132 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp20) {
1133 goto switch_7_exp_0;
1134 } else {
1135 {
1136#line 860
1137
1138#line 860
1139
1140#line 860
1141
1142#line 860
1143
1144#line 860
1145 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp24) {
1146 goto switch_7_exp_1;
1147 } else {
1148 {
1149#line 863
1150
1151#line 863
1152
1153#line 863
1154
1155#line 863
1156
1157#line 863
1158 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp28) {
1159 goto switch_7_exp_2;
1160 } else {
1161 {
1162#line 866
1163
1164#line 866
1165 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp29) {
1166 goto switch_7_exp_3;
1167 } else {
1168 {
1169#line 869
1170
1171#line 869
1172
1173#line 869
1174
1175#line 869
1176 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp32) {
1177 goto switch_7_exp_4;
1178 } else {
1179 {
1180#line 872
1181
1182#line 872
1183
1184#line 872
1185
1186#line 872
1187 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp35) {
1188 goto switch_7_exp_5;
1189 } else {
1190 {
1191#line 875
1192
1193#line 875
1194
1195#line 875
1196
1197#line 875
1198 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp38) {
1199 goto switch_7_exp_6;
1200 } else {
1201 {
1202#line 878
1203
1204#line 878
1205
1206#line 878
1207
1208#line 878
1209 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp41) {
1210 goto switch_7_exp_7;
1211 } else {
1212 {
1213#line 881
1214
1215#line 881
1216
1217#line 881
1218
1219#line 881
1220 if (irpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp44) {
1221 goto switch_7_exp_8;
1222 } else {
1223#line 884
1224 if (0) {
1225 switch_7_exp_0: ;
1226#line 886
1227 if (devExt__UpperConnectData__ClassService != 0) {
1228#line 887
1229 status = -1073741757;
1230 goto switch_7_break;
1231 } else {
1232#line 890
1233 if (irpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CONNECT_DATA) {
1234#line 891
1235 status = -1073741811;
1236 goto switch_7_break;
1237 }
1238 }
1239#line 897
1240 connectData = irpStack__Parameters__DeviceIoControl__Type3InputBuffer;
1241 goto switch_7_break;
1242 switch_7_exp_1:
1243#line 900
1244 status = -1073741822;
1245 goto switch_7_break;
1246 switch_7_exp_2: ;
1247#line 903
1248 if (irpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__INTERNAL_I8042_HOOK_KEYBOARD) {
1249#line 904
1250 status = -1073741811;
1251 goto switch_7_break;
1252 }
1253#line 909
1254 hookKeyboard = irpStack__Parameters__DeviceIoControl__Type3InputBuffer;
1255#line 910
1256 if (hookKeyboard__InitializationRoutine) {
1257
1258 }
1259#line 915
1260 if (hookKeyboard__IsrRoutine) {
1261
1262 }
1263#line 920
1264 status = 0;
1265 goto switch_7_break;
1266 switch_7_exp_3: ;
1267 switch_7_exp_4: ;
1268 switch_7_exp_5: ;
1269 switch_7_exp_6: ;
1270 switch_7_exp_7: ;
1271 switch_7_exp_8: ;
1272 goto switch_7_break;
1273 } else {
1274 switch_7_break: ;
1275 }
1276 }
1277 }
1278 }
1279 }
1280 }
1281 }
1282 }
1283 }
1284 }
1285 }
1286 }
1287 }
1288 }
1289 }
1290 }
1291 }
1292 }
1293 }
1294 {
1295#line 941
1296#line 941
1297 if (status < 0) {
1298 {
1299#line 943
1300 Irp__IoStatus__Status = status;
1301#line 944
1302 myStatus = status;
1303#line 945
1304 IofCompleteRequest(Irp, 0);
1305 }
1306#line 947
1307 return (status);
1308 }
1309 }
1310 {
1311#line 952
1312 tmp = KbFilter_DispatchPassThrough(DeviceObject, Irp);
1313 }
1314#line 954
1315 return (tmp);
1316}
1317}
1318
1319void errorFn(void)
1320{
1321
1322 {
1323 goto ERROR;
1324 ERROR:
1325#line 29
1326 return;
1327}
1328}