1int FloppyThread ;
2int KernelMode ;
3int Suspended ;
4int Executive ;
5int DiskController ;
6int FloppyDiskPeripheral ;
7int FlConfigCallBack ;
8int MaximumInterfaceType ;
9int MOUNTDEV_MOUNTED_DEVICE_GUID ;
10int myStatus ;
11int s ;
12int UNLOADED ;
13int NP ;
14int DC ;
15int SKIP1 ;
16int SKIP2 ;
17int MPR1 ;
18int MPR3 ;
19int IPC ;
20int pended ;
21int compRegistered ;
22int lowerDriverReturn ;
23int setEventCalled ;
24int customIrp ;
25
26void errorFn(void)
27{
28
29 {
30 goto ERROR;
31 ERROR:
32 return;
33}
34}
35
36void _BLAST_init(void)
37{
38
39 {
40#line 73
41 UNLOADED = 0;
42#line 74
43 NP = 1;
44#line 75
45 DC = 2;
46#line 76
47 SKIP1 = 3;
48#line 77
49 SKIP2 = 4;
50#line 78
51 MPR1 = 5;
52#line 79
53 MPR3 = 6;
54#line 80
55 IPC = 7;
56#line 81
57 s = UNLOADED;
58#line 82
59 pended = 0;
60#line 83
61 compRegistered = 0;
62#line 84
63 lowerDriverReturn = 0;
64#line 85
65 setEventCalled = 0;
66#line 86
67 customIrp = 0;
68#line 87
69 return;
70}
71}
72#line 90 "floppy_simpl3.cil.c"
73int PagingReferenceCount = 0;
74#line 91 "floppy_simpl3.cil.c"
75int PagingMutex = 0;
76#line 92 "floppy_simpl3.cil.c"
77int FlAcpiConfigureFloppy(int DisketteExtension , int FdcInfo )
78{
79
80 {
81#line 96
82 return (0);
83}
84}
85#line 99 "floppy_simpl3.cil.c"
86int FlQueueIrpToThread(int Irp , int DisketteExtension )
87{ int status ;
88 int threadHandle ;
89 int DisketteExtension__PoweringDown ;
90 int DisketteExtension__ThreadReferenceCount ;
91 int DisketteExtension__FloppyThread ;
92 int Irp__IoStatus__Status ;
93 int Irp__IoStatus__Information ;
94 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
95 int ObjAttributes ;
96 int __cil_tmp12 ;
97 int __cil_tmp13 ;
98
99 {
100#line 111
101 if (DisketteExtension__PoweringDown == 1) {
102#line 112
103 myStatus = -1073741101;
104#line 113
105 Irp__IoStatus__Status = -1073741101;
106#line 114
107 Irp__IoStatus__Information = 0;
108#line 115
109 return (-1073741101);
110 }
111#line 119
112 DisketteExtension__ThreadReferenceCount ++;
113#line 120
114 if (DisketteExtension__ThreadReferenceCount == 0) {
115#line 121
116 DisketteExtension__ThreadReferenceCount ++;
117#line 122
118 PagingReferenceCount ++;
119#line 123
120 if (PagingReferenceCount == 1) {
121
122 }
123 {
124#line 129
125 status = PsCreateSystemThread(threadHandle, 0, ObjAttributes, 0, 0, FloppyThread,
126 DisketteExtension);
127 }
128 {
129#line 132
130#line 132
131 if (status < 0) {
132#line 133
133 DisketteExtension__ThreadReferenceCount = -1;
134#line 134
135 PagingReferenceCount --;
136#line 135
137 if (PagingReferenceCount == 0) {
138
139 }
140#line 140
141 return (status);
142 }
143 }
144 {
145#line 145
146 status = ObReferenceObjectByHandle(threadHandle, 1048576, 0, KernelMode, DisketteExtension__FloppyThread,
147 0);
148#line 147
149 ZwClose(threadHandle);
150 }
151 {
152#line 149
153#line 149
154 if (status < 0) {
155#line 150
156 return (status);
157 }
158 }
159 }
160#line 157
161
162#line 158
163 if (pended == 0) {
164#line 159
165 pended = 1;
166 } else {
167 {
168#line 162
169 errorFn();
170 }
171 }
172#line 165
173 return (259);
174}
175}
176#line 168 "floppy_simpl3.cil.c"
177int FloppyPnp(int DeviceObject , int Irp )
178{ int DeviceObject__DeviceExtension ;
179 int Irp__Tail__Overlay__CurrentStackLocation ;
180 int Irp__IoStatus__Information ;
181 int Irp__IoStatus__Status ;
182 int Irp__CurrentLocation ;
183 int disketteExtension__IsRemoved ;
184 int disketteExtension__IsStarted ;
185 int disketteExtension__TargetObject ;
186 int disketteExtension__HoldNewRequests ;
187 int disketteExtension__FloppyThread ;
188 int disketteExtension__InterfaceString__Buffer ;
189 int disketteExtension__InterfaceString ;
190 int disketteExtension__ArcName__Length ;
191 int disketteExtension__ArcName ;
192 int irpSp__MinorFunction ;
193 int IoGetConfigurationInformation__FloppyCount ;
194 int irpSp ;
195 int disketteExtension ;
196 int ntStatus ;
197 int doneEvent ;
198 int irpSp___0 ;
199 int nextIrpSp ;
200 int nextIrpSp__Control ;
201 int irpSp___1 ;
202 int irpSp__Context ;
203 int irpSp__Control ;
204 long __cil_tmp29 ;
205 long __cil_tmp30 ;
206
207 {
208#line 197
209 ntStatus = 0;
210#line 198
211 PagingReferenceCount ++;
212#line 199
213 if (PagingReferenceCount == 1) {
214
215 }
216#line 204
217 disketteExtension = DeviceObject__DeviceExtension;
218#line 205
219 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
220#line 206
221 if (disketteExtension__IsRemoved) {
222 {
223#line 208
224 Irp__IoStatus__Information = 0;
225#line 209
226 Irp__IoStatus__Status = -1073741738;
227#line 210
228 myStatus = -1073741738;
229#line 211
230 IofCompleteRequest(Irp, 0);
231 }
232#line 213
233 return (-1073741738);
234 }
235#line 217
236 if (irpSp__MinorFunction == 0) {
237 goto switch_0_0;
238 } else {
239#line 220
240 if (irpSp__MinorFunction == 5) {
241 goto switch_0_5;
242 } else {
243#line 223
244 if (irpSp__MinorFunction == 1) {
245 goto switch_0_5;
246 } else {
247#line 226
248 if (irpSp__MinorFunction == 6) {
249 goto switch_0_6;
250 } else {
251#line 229
252 if (irpSp__MinorFunction == 3) {
253 goto switch_0_6;
254 } else {
255#line 232
256 if (irpSp__MinorFunction == 4) {
257 goto switch_0_4;
258 } else {
259#line 235
260 if (irpSp__MinorFunction == 2) {
261 goto switch_0_2;
262 } else {
263 goto switch_0_default;
264#line 240
265 if (0) {
266 switch_0_0:
267 {
268#line 243
269 ntStatus = FloppyStartDevice(DeviceObject, Irp);
270 }
271 goto switch_0_break;
272 switch_0_5:
273#line 248
274 if (irpSp__MinorFunction == 5) {
275
276 }
277#line 253
278 if (! disketteExtension__IsStarted) {
279#line 254
280 if (s == NP) {
281#line 255
282 s = SKIP1;
283 } else {
284 {
285#line 258
286 errorFn();
287 }
288 }
289 {
290#line 262
291 Irp__CurrentLocation ++;
292#line 263
293 Irp__Tail__Overlay__CurrentStackLocation ++;
294#line 264
295 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
296 }
297#line 266
298 return (ntStatus);
299 }
300 {
301#line 271
302 disketteExtension__HoldNewRequests = 1;
303#line 272
304 ntStatus = FlQueueIrpToThread(Irp, disketteExtension);
305 }
306 {
307#line 274
308 __cil_tmp29 = (long )ntStatus;
309#line 274
310 if (__cil_tmp29 == 259L) {
311 {
312#line 276
313 KeWaitForSingleObject(disketteExtension__FloppyThread, Executive,
314 KernelMode, 0, 0);
315 }
316#line 279
317 if (disketteExtension__FloppyThread != 0) {
318
319 }
320#line 284
321 disketteExtension__FloppyThread = 0;
322#line 285
323 Irp__IoStatus__Status = 0;
324#line 286
325 myStatus = 0;
326#line 287
327 if (s == NP) {
328#line 288
329 s = SKIP1;
330 } else {
331 {
332#line 291
333 errorFn();
334 }
335 }
336 {
337#line 295
338 Irp__CurrentLocation ++;
339#line 296
340 Irp__Tail__Overlay__CurrentStackLocation ++;
341#line 297
342 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
343 }
344 } else {
345 {
346#line 301
347 ntStatus = -1073741823;
348#line 302
349 Irp__IoStatus__Status = ntStatus;
350#line 303
351 myStatus = ntStatus;
352#line 304
353 Irp__IoStatus__Information = 0;
354#line 305
355 IofCompleteRequest(Irp, 0);
356 }
357 }
358 }
359 goto switch_0_break;
360 switch_0_6:
361#line 311
362 if (irpSp__MinorFunction == 6) {
363
364 }
365#line 316
366 if (! disketteExtension__IsStarted) {
367#line 317
368 Irp__IoStatus__Status = 0;
369#line 318
370 myStatus = 0;
371#line 319
372 if (s == NP) {
373#line 320
374 s = SKIP1;
375 } else {
376 {
377#line 323
378 errorFn();
379 }
380 }
381 {
382#line 327
383 Irp__CurrentLocation ++;
384#line 328
385 Irp__Tail__Overlay__CurrentStackLocation ++;
386#line 329
387 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
388 }
389 } else {
390#line 332
391 Irp__IoStatus__Status = 0;
392#line 333
393 myStatus = 0;
394#line 334
395 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
396#line 335
397 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
398#line 336
399 nextIrpSp__Control = 0;
400#line 337
401 if (s != NP) {
402 {
403#line 339
404 errorFn();
405 }
406 } else {
407#line 342
408 if (compRegistered != 0) {
409 {
410#line 344
411 errorFn();
412 }
413 } else {
414#line 347
415 compRegistered = 1;
416 }
417 }
418 {
419#line 351
420 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
421#line 352
422 irpSp__Context = doneEvent;
423#line 353
424 irpSp__Control = 224;
425#line 357
426 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
427 }
428 {
429#line 359
430 __cil_tmp30 = (long )ntStatus;
431#line 359
432 if (__cil_tmp30 == 259L) {
433 {
434#line 361
435 KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
436#line 362
437 ntStatus = myStatus;
438 }
439 }
440 }
441 {
442#line 368
443 disketteExtension__HoldNewRequests = 0;
444#line 369
445 Irp__IoStatus__Status = ntStatus;
446#line 370
447 myStatus = ntStatus;
448#line 371
449 Irp__IoStatus__Information = 0;
450#line 372
451 IofCompleteRequest(Irp, 0);
452 }
453 }
454 goto switch_0_break;
455 switch_0_4:
456#line 377
457 disketteExtension__IsStarted = 0;
458#line 378
459 Irp__IoStatus__Status = 0;
460#line 379
461 myStatus = 0;
462#line 380
463 if (s == NP) {
464#line 381
465 s = SKIP1;
466 } else {
467 {
468#line 384
469 errorFn();
470 }
471 }
472 {
473#line 388
474 Irp__CurrentLocation ++;
475#line 389
476 Irp__Tail__Overlay__CurrentStackLocation ++;
477#line 390
478 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
479 }
480 goto switch_0_break;
481 switch_0_2:
482#line 394
483 disketteExtension__HoldNewRequests = 0;
484#line 395
485 disketteExtension__IsStarted = 0;
486#line 396
487 disketteExtension__IsRemoved = 1;
488#line 397
489 if (s == NP) {
490#line 398
491 s = SKIP1;
492 } else {
493 {
494#line 401
495 errorFn();
496 }
497 }
498 {
499#line 405
500 Irp__CurrentLocation ++;
501#line 406
502 Irp__Tail__Overlay__CurrentStackLocation ++;
503#line 407
504 Irp__IoStatus__Status = 0;
505#line 408
506 myStatus = 0;
507#line 409
508 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
509 }
510#line 411
511 if (disketteExtension__InterfaceString__Buffer != 0) {
512 {
513#line 413
514 IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
515 0);
516 }
517 }
518#line 419
519 if (disketteExtension__ArcName__Length != 0) {
520 {
521#line 421
522 IoDeleteSymbolicLink(disketteExtension__ArcName);
523 }
524 }
525#line 426
526 IoGetConfigurationInformation__FloppyCount --;
527 goto switch_0_break;
528 switch_0_default: ;
529#line 429
530 if (s == NP) {
531#line 430
532 s = SKIP1;
533 } else {
534 {
535#line 433
536 errorFn();
537 }
538 }
539 {
540#line 437
541 Irp__CurrentLocation ++;
542#line 438
543 Irp__Tail__Overlay__CurrentStackLocation ++;
544#line 439
545 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
546 }
547 } else {
548 switch_0_break: ;
549 }
550 }
551 }
552 }
553 }
554 }
555 }
556 }
557#line 452
558 PagingReferenceCount --;
559#line 453
560 if (PagingReferenceCount == 0) {
561
562 }
563#line 458
564 return (ntStatus);
565}
566}
567#line 461 "floppy_simpl3.cil.c"
568int FloppyStartDevice(int DeviceObject , int Irp )
569{ int DeviceObject__DeviceExtension ;
570 int Irp__Tail__Overlay__CurrentStackLocation ;
571 int Irp__IoStatus__Status ;
572 int disketteExtension__TargetObject ;
573 int disketteExtension__MaxTransferSize ;
574 int disketteExtension__DriveType ;
575 int disketteExtension__PerpendicularMode ;
576 int disketteExtension__DeviceUnit ;
577 int disketteExtension__DriveOnValue ;
578 int disketteExtension__UnderlyingPDO ;
579 int disketteExtension__InterfaceString ;
580 int disketteExtension__IsStarted ;
581 int disketteExtension__HoldNewRequests ;
582 int ntStatus ;
583 int pnpStatus ;
584 int doneEvent ;
585 int fdcInfo ;
586 int fdcInfo__BufferCount ;
587 int fdcInfo__BufferSize ;
588 int fdcInfo__MaxTransferSize ;
589 int fdcInfo__AcpiBios ;
590 int fdcInfo__AcpiFdiSupported ;
591 int fdcInfo__PeripheralNumber ;
592 int fdcInfo__BusType ;
593 int fdcInfo__ControllerNumber ;
594 int fdcInfo__UnitNumber ;
595 int fdcInfo__BusNumber ;
596 int Dc ;
597 int Fp ;
598 int disketteExtension ;
599 int irpSp ;
600 int irpSp___0 ;
601 int nextIrpSp ;
602 int nextIrpSp__Control ;
603 int irpSp___1 ;
604 int irpSp__Control ;
605 int irpSp__Context ;
606 int InterfaceType ;
607 int KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 ;
608 long __cil_tmp42 ;
609 int __cil_tmp43 ;
610 int __cil_tmp44 ;
611 int __cil_tmp45 ;
612 int __cil_tmp46 ;
613 int __cil_tmp47 ;
614 int __cil_tmp48 ;
615 int __cil_tmp49 ;
616
617 {
618#line 503
619 Dc = DiskController;
620#line 504
621 Fp = FloppyDiskPeripheral;
622#line 505
623 disketteExtension = DeviceObject__DeviceExtension;
624#line 506
625 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
626#line 507
627 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
628#line 508
629 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
630#line 509
631 nextIrpSp__Control = 0;
632#line 510
633 if (s != NP) {
634 {
635#line 512
636 errorFn();
637 }
638 } else {
639#line 515
640 if (compRegistered != 0) {
641 {
642#line 517
643 errorFn();
644 }
645 } else {
646#line 520
647 compRegistered = 1;
648 }
649 }
650 {
651#line 524
652 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
653#line 525
654 irpSp__Context = doneEvent;
655#line 526
656 irpSp__Control = 224;
657#line 530
658 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
659 }
660 {
661#line 532
662 __cil_tmp42 = (long )ntStatus;
663#line 532
664 if (__cil_tmp42 == 259L) {
665 {
666#line 534
667 ntStatus = KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
668#line 535
669 ntStatus = myStatus;
670 }
671 }
672 }
673 {
674#line 541
675 fdcInfo__BufferCount = 0;
676#line 542
677 fdcInfo__BufferSize = 0;
678#line 543
679 __cil_tmp43 = 3080;
680#line 543
681 __cil_tmp44 = 458752;
682#line 543
683 __cil_tmp45 = 461832;
684#line 543
685 __cil_tmp46 = 461835;
686#line 543
687 ntStatus = FlFdcDeviceIo(disketteExtension__TargetObject, __cil_tmp46, fdcInfo);
688 }
689#line 546
690 if (ntStatus >= 0) {
691#line 547
692 disketteExtension__MaxTransferSize = fdcInfo__MaxTransferSize;
693#line 548
694 if (fdcInfo__AcpiBios) {
695#line 549
696 if (fdcInfo__AcpiFdiSupported) {
697 {
698#line 551
699 ntStatus = FlAcpiConfigureFloppy(disketteExtension, fdcInfo);
700 }
701#line 553
702 if (disketteExtension__DriveType == 4) {
703#line 554
704 __cil_tmp47 = uninf1();
705#line 554
706
707 }
708 } else {
709 goto _L;
710 }
711 } else {
712 _L:
713#line 563
714 if (disketteExtension__DriveType == 4) {
715#line 564
716 __cil_tmp48 = uninf1();
717#line 564
718
719 }
720#line 568
721 InterfaceType = 0;
722 {
723#line 570
724 while (1) {
725 while_0_continue: ;
726
727#line 572
728 if (InterfaceType >= MaximumInterfaceType) {
729 goto while_1_break;
730 }
731 {
732#line 578
733 fdcInfo__BusType = InterfaceType;
734#line 579
735 ntStatus = IoQueryDeviceDescription(fdcInfo__BusType, fdcInfo__BusNumber,
736 Dc, fdcInfo__ControllerNumber, Fp, fdcInfo__PeripheralNumber,
737 FlConfigCallBack, disketteExtension);
738 }
739#line 583
740 if (ntStatus >= 0) {
741 goto while_1_break;
742 }
743#line 588
744 InterfaceType ++;
745 }
746 while_0_break: ;
747 }
748 while_1_break: ;
749 }
750#line 593
751 if (ntStatus >= 0) {
752#line 594
753 if (KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 != 0) {
754#line 595
755 disketteExtension__DeviceUnit = fdcInfo__UnitNumber;
756#line 596
757
758 } else {
759#line 598
760 disketteExtension__DeviceUnit = fdcInfo__PeripheralNumber;
761#line 599
762
763#line 599
764
765 }
766 {
767#line 602
768 pnpStatus = IoRegisterDeviceInterface(disketteExtension__UnderlyingPDO, MOUNTDEV_MOUNTED_DEVICE_GUID,
769 0, disketteExtension__InterfaceString);
770 }
771#line 605
772 if (pnpStatus >= 0) {
773 {
774#line 607
775 pnpStatus = IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
776 1);
777 }
778 }
779#line 613
780 disketteExtension__IsStarted = 1;
781#line 614
782 disketteExtension__HoldNewRequests = 0;
783 }
784 }
785 {
786#line 622
787 Irp__IoStatus__Status = ntStatus;
788#line 623
789 myStatus = ntStatus;
790#line 624
791 IofCompleteRequest(Irp, 0);
792 }
793#line 626
794 return (ntStatus);
795}
796}
797#line 629 "floppy_simpl3.cil.c"
798int FloppyPnpComplete(int DeviceObject , int Irp , int Context )
799{
800
801 {
802 {
803#line 634
804 KeSetEvent(Context, 1, 0);
805 }
806#line 636
807 return (-1073741802);
808}
809}
810#line 639 "floppy_simpl3.cil.c"
811int FlFdcDeviceIo(int DeviceObject , int Ioctl , int Data )
812{ int ntStatus ;
813 int irp ;
814 int irpStack ;
815 int doneEvent ;
816 int ioStatus ;
817 int irp__Tail__Overlay__CurrentStackLocation ;
818 int irpStack__Parameters__DeviceIoControl__Type3InputBuffer ;
819 long __cil_tmp11 ;
820
821 {
822 {
823#line 650
824 irp = IoBuildDeviceIoControlRequest(Ioctl, DeviceObject, 0, 0, 0, 0, 1, doneEvent,
825 ioStatus);
826 }
827#line 653
828 if (irp == 0) {
829#line 654
830 return (-1073741670);
831 }
832 {
833#line 659
834 irpStack = irp__Tail__Overlay__CurrentStackLocation - 1;
835#line 660
836 irpStack__Parameters__DeviceIoControl__Type3InputBuffer = Data;
837#line 661
838 ntStatus = IofCallDriver(DeviceObject, irp);
839 }
840 {
841#line 663
842 __cil_tmp11 = (long )ntStatus;
843#line 663
844 if (__cil_tmp11 == 259L) {
845 {
846#line 665
847 KeWaitForSingleObject(doneEvent, Suspended, KernelMode, 0, 0);
848#line 666
849 ntStatus = myStatus;
850 }
851 }
852 }
853#line 671
854 return (ntStatus);
855}
856}
857#line 674 "floppy_simpl3.cil.c"
858void FloppyProcessQueuedRequests(int DisketteExtension )
859{
860
861 {
862#line 678
863 return;
864}
865}
866#line 681 "floppy_simpl3.cil.c"
867void stub_driver_init(void)
868{
869
870 {
871#line 685
872 s = NP;
873#line 686
874 pended = 0;
875#line 687
876 compRegistered = 0;
877#line 688
878 lowerDriverReturn = 0;
879#line 689
880 setEventCalled = 0;
881#line 690
882 customIrp = 0;
883#line 691
884 return;
885}
886}
887#line 694 "floppy_simpl3.cil.c"
888int main(void)
889{ int status ;
890 int irp ;
891 int pirp ;
892 int pirp__IoStatus__Status ;
893
894 int irp_choice ;
895 int devobj ;
896 int __cil_tmp8 ;
897
898 FloppyThread = 0;
899 KernelMode = 0;
900 Suspended = 0;
901 Executive = 0;
902 DiskController = 0;
903 FloppyDiskPeripheral = 0;
904 FlConfigCallBack = 0;
905 MaximumInterfaceType = 0;
906 MOUNTDEV_MOUNTED_DEVICE_GUID = 0;
907 myStatus = 0;
908 s = 0;
909 UNLOADED = 0;
910 NP = 0;
911 DC = 0;
912 SKIP1 = 0;
913 SKIP2 = 0;
914 MPR1 = 0;
915 MPR3 = 0;
916 IPC = 0;
917 pended = 0;
918 compRegistered = 0;
919 lowerDriverReturn = 0;
920 setEventCalled = 0;
921 customIrp = 0;
922
923 {
924 {
925#line 705
926 status = 0;
927#line 706
928 pirp = irp;
929#line 707
930 _BLAST_init();
931 }
932#line 709
933 if (status >= 0) {
934#line 710
935 s = NP;
936#line 711
937 customIrp = 0;
938#line 712
939 setEventCalled = customIrp;
940#line 713
941 lowerDriverReturn = setEventCalled;
942#line 714
943 compRegistered = lowerDriverReturn;
944#line 715
945 pended = compRegistered;
946#line 716
947 pirp__IoStatus__Status = 0;
948#line 717
949 myStatus = 0;
950#line 718
951 if (irp_choice == 0) {
952#line 719
953 pirp__IoStatus__Status = -1073741637;
954#line 720
955 myStatus = -1073741637;
956 }
957 {
958#line 725
959 stub_driver_init();
960 }
961 {
962#line 727
963#line 727
964 if (status < 0) {
965#line 728
966 return (-1);
967 }
968 }
969#line 732
970 int tmp_ndt_1;
971 tmp_ndt_1 = __VERIFIER_nondet_int();
972 if (tmp_ndt_1 == 3) {
973 goto switch_2_3;
974 } else {
975 goto switch_2_default;
976#line 737
977 if (0) {
978 switch_2_3:
979 {
980#line 740
981 status = FloppyPnp(devobj, pirp);
982 }
983 goto switch_2_break;
984 switch_2_default: ;
985#line 744
986 return (-1);
987 } else {
988 switch_2_break: ;
989 }
990 }
991 }
992#line 753
993 if (pended == 1) {
994#line 754
995 if (s == NP) {
996#line 755
997 s = NP;
998 } else {
999 goto _L___2;
1000 }
1001 } else {
1002 _L___2:
1003#line 761
1004 if (pended == 1) {
1005#line 762
1006 if (s == MPR3) {
1007#line 763
1008 s = MPR3;
1009 } else {
1010 goto _L___1;
1011 }
1012 } else {
1013 _L___1:
1014#line 769
1015 if (s != UNLOADED) {
1016#line 772
1017 if (status != -1) {
1018#line 775
1019 if (s != SKIP2) {
1020#line 776
1021 if (s != IPC) {
1022#line 777
1023 if (s != DC) {
1024 {
1025#line 779
1026 errorFn();
1027 }
1028 } else {
1029 goto _L___0;
1030 }
1031 } else {
1032 goto _L___0;
1033 }
1034 } else {
1035 _L___0:
1036#line 789
1037 if (pended == 1) {
1038#line 790
1039 if (status != 259) {
1040#line 791
1041 status = 0;
1042 }
1043 } else {
1044#line 796
1045 if (s == DC) {
1046#line 797
1047 if (status == 259) {
1048 {
1049#line 799
1050 errorFn();
1051 }
1052 }
1053 } else {
1054#line 805
1055 if (status != lowerDriverReturn) {
1056 {
1057#line 807
1058 errorFn();
1059 }
1060 }
1061 }
1062 }
1063 }
1064 }
1065 }
1066 }
1067 }
1068#line 819
1069 status = 0;
1070#line 820
1071 return (status);
1072}
1073}
1074#line 823 "floppy_simpl3.cil.c"
1075int IoBuildDeviceIoControlRequest(int IoControlCode , int DeviceObject , int InputBuffer ,
1076 int InputBufferLength , int OutputBuffer , int OutputBufferLength ,
1077 int InternalDeviceIoControl , int Event , int IoStatusBlock )
1078{
1079 int malloc ;
1080
1081 {
1082#line 830
1083 customIrp = 1;
1084#line 831
1085 int tmp_ndt_2;
1086 tmp_ndt_2 = __VERIFIER_nondet_int();
1087 if (tmp_ndt_2 == 0) {
1088 goto switch_3_0;
1089 } else {
1090 goto switch_3_default;
1091#line 836
1092 if (0) {
1093 switch_3_0:
1094#line 838
1095 return (malloc);
1096 switch_3_default: ;
1097#line 840
1098 return (0);
1099 } else {
1100
1101 }
1102 }
1103}
1104}
1105#line 848 "floppy_simpl3.cil.c"
1106int IoDeleteSymbolicLink(int SymbolicLinkName )
1107{
1108
1109 {
1110#line 852
1111 int tmp_ndt_3;
1112 tmp_ndt_3 = __VERIFIER_nondet_int();
1113 if (tmp_ndt_3 == 0) {
1114 goto switch_4_0;
1115 } else {
1116 goto switch_4_default;
1117#line 857
1118 if (0) {
1119 switch_4_0:
1120#line 859
1121 return (0);
1122 switch_4_default: ;
1123#line 861
1124 return (-1073741823);
1125 } else {
1126
1127 }
1128 }
1129}
1130}
1131#line 869 "floppy_simpl3.cil.c"
1132int IoQueryDeviceDescription(int BusType , int BusNumber , int ControllerType , int ControllerNumber ,
1133 int PeripheralType , int PeripheralNumber , int CalloutRoutine ,
1134 int Context )
1135{
1136
1137 {
1138#line 875
1139 int tmp_ndt_4;
1140 tmp_ndt_4 = __VERIFIER_nondet_int();
1141 if (tmp_ndt_4 == 0) {
1142 goto switch_5_0;
1143 } else {
1144 goto switch_5_default;
1145#line 880
1146 if (0) {
1147 switch_5_0:
1148#line 882
1149 return (0);
1150 switch_5_default: ;
1151#line 884
1152 return (-1073741823);
1153 } else {
1154
1155 }
1156 }
1157}
1158}
1159#line 892 "floppy_simpl3.cil.c"
1160int IoRegisterDeviceInterface(int PhysicalDeviceObject , int InterfaceClassGuid ,
1161 int ReferenceString , int SymbolicLinkName )
1162{
1163
1164 {
1165#line 897
1166 int tmp_ndt_5;
1167 tmp_ndt_5 = __VERIFIER_nondet_int();
1168 if (tmp_ndt_5 == 0) {
1169 goto switch_6_0;
1170 } else {
1171 goto switch_6_default;
1172#line 902
1173 if (0) {
1174 switch_6_0:
1175#line 904
1176 return (0);
1177 switch_6_default: ;
1178#line 906
1179 return (-1073741808);
1180 } else {
1181
1182 }
1183 }
1184}
1185}
1186#line 914 "floppy_simpl3.cil.c"
1187int IoSetDeviceInterfaceState(int SymbolicLinkName , int Enable )
1188{
1189
1190 {
1191#line 918
1192 int tmp_ndt_6;
1193 tmp_ndt_6 = __VERIFIER_nondet_int();
1194 if (tmp_ndt_6 == 0) {
1195 goto switch_7_0;
1196 } else {
1197 goto switch_7_default;
1198#line 923
1199 if (0) {
1200 switch_7_0:
1201#line 925
1202 return (0);
1203 switch_7_default: ;
1204#line 927
1205 return (-1073741823);
1206 } else {
1207
1208 }
1209 }
1210}
1211}
1212#line 935 "floppy_simpl3.cil.c"
1213void stubMoreProcessingRequired(void)
1214{
1215
1216 {
1217#line 939
1218 if (s == NP) {
1219#line 940
1220 s = MPR1;
1221 } else {
1222 {
1223#line 943
1224 errorFn();
1225 }
1226 }
1227#line 946
1228 return;
1229}
1230}
1231#line 949 "floppy_simpl3.cil.c"
1232int IofCallDriver(int DeviceObject , int Irp )
1233{
1234 int returnVal2 ;
1235 int compRetStatus1 ;
1236 int lcontext ;
1237 unsigned long __cil_tmp7 ;
1238
1239 {
1240#line 956
1241 if (compRegistered) {
1242 {
1243#line 958
1244 compRetStatus1 = FloppyPnpComplete(DeviceObject, Irp, lcontext);
1245 }
1246 {
1247#line 960
1248 __cil_tmp7 = (unsigned long )compRetStatus1;
1249#line 960
1250 if (__cil_tmp7 == -1073741802) {
1251 {
1252#line 962
1253 stubMoreProcessingRequired();
1254 }
1255 }
1256 }
1257 }
1258#line 970
1259 int tmp_ndt_7;
1260 tmp_ndt_7 = __VERIFIER_nondet_int();
1261 if (tmp_ndt_7 == 0) {
1262 goto switch_8_0;
1263 } else {
1264#line 973
1265 int tmp_ndt_8;
1266 tmp_ndt_8 = __VERIFIER_nondet_int();
1267 if (tmp_ndt_8 == 1) {
1268 goto switch_8_1;
1269 } else {
1270 goto switch_8_default;
1271#line 978
1272 if (0) {
1273 switch_8_0:
1274#line 980
1275 returnVal2 = 0;
1276 goto switch_8_break;
1277 switch_8_1:
1278#line 983
1279 returnVal2 = -1073741823;
1280 goto switch_8_break;
1281 switch_8_default:
1282#line 986
1283 returnVal2 = 259;
1284 goto switch_8_break;
1285 } else {
1286 switch_8_break: ;
1287 }
1288 }
1289 }
1290#line 994
1291 if (s == NP) {
1292#line 995
1293 s = IPC;
1294#line 996
1295 lowerDriverReturn = returnVal2;
1296 } else {
1297#line 998
1298 if (s == MPR1) {
1299#line 999
1300 if (returnVal2 == 259) {
1301#line 1000
1302 s = MPR3;
1303#line 1001
1304 lowerDriverReturn = returnVal2;
1305 } else {
1306#line 1003
1307 s = NP;
1308#line 1004
1309 lowerDriverReturn = returnVal2;
1310 }
1311 } else {
1312#line 1007
1313 if (s == SKIP1) {
1314#line 1008
1315 s = SKIP2;
1316#line 1009
1317 lowerDriverReturn = returnVal2;
1318 } else {
1319 {
1320#line 1012
1321 errorFn();
1322 }
1323 }
1324 }
1325 }
1326#line 1017
1327 return (returnVal2);
1328}
1329}
1330#line 1020 "floppy_simpl3.cil.c"
1331void IofCompleteRequest(int Irp , int PriorityBoost )
1332{
1333
1334 {
1335#line 1024
1336 if (s == NP) {
1337#line 1025
1338 s = DC;
1339 } else {
1340 {
1341#line 1028
1342 errorFn();
1343 }
1344 }
1345#line 1031
1346 return;
1347}
1348}
1349#line 1034 "floppy_simpl3.cil.c"
1350int KeSetEvent(int Event , int Increment , int Wait )
1351{ int l ;
1352
1353 {
1354#line 1038
1355 setEventCalled = 1;
1356#line 1039
1357 return (l);
1358}
1359}
1360#line 1042 "floppy_simpl3.cil.c"
1361int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
1362 int Timeout )
1363{
1364
1365 {
1366#line 1047
1367 if (s == MPR3) {
1368#line 1048
1369 if (setEventCalled == 1) {
1370#line 1049
1371 s = NP;
1372#line 1050
1373 setEventCalled = 0;
1374 } else {
1375 goto _L;
1376 }
1377 } else {
1378 _L:
1379#line 1056
1380 if (customIrp == 1) {
1381#line 1057
1382 s = NP;
1383#line 1058
1384 customIrp = 0;
1385 } else {
1386#line 1060
1387 if (s == MPR3) {
1388 {
1389#line 1062
1390 errorFn();
1391 }
1392 }
1393 }
1394 }
1395#line 1069
1396 int tmp_ndt_9;
1397 tmp_ndt_9 = __VERIFIER_nondet_int();
1398 if (tmp_ndt_9 == 0) {
1399 goto switch_9_0;
1400 } else {
1401 goto switch_9_default;
1402#line 1074
1403 if (0) {
1404 switch_9_0:
1405#line 1076
1406 return (0);
1407 switch_9_default: ;
1408#line 1078
1409 return (-1073741823);
1410 } else {
1411
1412 }
1413 }
1414}
1415}
1416#line 1086 "floppy_simpl3.cil.c"
1417int ObReferenceObjectByHandle(int Handle , int DesiredAccess , int ObjectType , int AccessMode ,
1418 int Object , int HandleInformation )
1419{
1420
1421 {
1422#line 1091
1423 int tmp_ndt_10;
1424 tmp_ndt_10 = __VERIFIER_nondet_int();
1425 if (tmp_ndt_10 == 0) {
1426 goto switch_10_0;
1427 } else {
1428 goto switch_10_default;
1429#line 1096
1430 if (0) {
1431 switch_10_0:
1432#line 1098
1433 return (0);
1434 switch_10_default: ;
1435#line 1100
1436 return (-1073741823);
1437 } else {
1438
1439 }
1440 }
1441}
1442}
1443#line 1108 "floppy_simpl3.cil.c"
1444int PsCreateSystemThread(int ThreadHandle , int DesiredAccess , int ObjectAttributes ,
1445 int ProcessHandle , int ClientId , int StartRoutine , int StartContext )
1446{
1447
1448 {
1449#line 1113
1450 int tmp_ndt_11;
1451 tmp_ndt_11 = __VERIFIER_nondet_int();
1452 if (tmp_ndt_11 == 0) {
1453 goto switch_11_0;
1454 } else {
1455 goto switch_11_default;
1456#line 1118
1457 if (0) {
1458 switch_11_0:
1459#line 1120
1460 return (0);
1461 switch_11_default: ;
1462#line 1122
1463 return (-1073741823);
1464 } else {
1465
1466 }
1467 }
1468}
1469}
1470#line 1130 "floppy_simpl3.cil.c"
1471int ZwClose(int Handle )
1472{
1473
1474 {
1475#line 1134
1476 int tmp_ndt_12;
1477 tmp_ndt_12 = __VERIFIER_nondet_int();
1478 if (tmp_ndt_12 == 0) {
1479 goto switch_12_0;
1480 } else {
1481 goto switch_12_default;
1482#line 1139
1483 if (0) {
1484 switch_12_0:
1485#line 1141
1486 return (0);
1487 switch_12_default: ;
1488#line 1143
1489 return (-1073741823);
1490 } else {
1491
1492 }
1493 }
1494}
1495}
1496#line 1151 "floppy_simpl3.cil.c"
1497int FloppyCreateClose(int DeviceObject , int Irp )
1498{ int Irp__IoStatus__Status ;
1499 int Irp__IoStatus__Information ;
1500
1501 {
1502 {
1503#line 1157
1504 myStatus = 0;
1505#line 1158
1506 Irp__IoStatus__Status = 0;
1507#line 1159
1508 Irp__IoStatus__Information = 1;
1509#line 1160
1510 IofCompleteRequest(Irp, 0);
1511 }
1512#line 1162
1513 return (0);
1514}
1515}