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 FloppyThread ;
9int KernelMode ;
10int Suspended ;
11int Executive ;
12int DiskController ;
13int FloppyDiskPeripheral ;
14int FlConfigCallBack ;
15int MaximumInterfaceType ;
16int MOUNTDEV_MOUNTED_DEVICE_GUID ;
17int myStatus ;
18int s ;
19int UNLOADED ;
20int NP ;
21int DC ;
22int SKIP1 ;
23int SKIP2 ;
24int MPR1 ;
25int MPR3 ;
26int IPC ;
27int pended ;
28int compRegistered ;
29int lowerDriverReturn ;
30int setEventCalled ;
31int customIrp ;
32
33void _BLAST_init(void)
34{
35
36 {
37#line 75
38 UNLOADED = 0;
39#line 76
40 NP = 1;
41#line 77
42 DC = 2;
43#line 78
44 SKIP1 = 3;
45#line 79
46 SKIP2 = 4;
47#line 80
48 MPR1 = 5;
49#line 81
50 MPR3 = 6;
51#line 82
52 IPC = 7;
53#line 83
54 s = UNLOADED;
55#line 84
56 pended = 0;
57#line 85
58 compRegistered = 0;
59#line 86
60 lowerDriverReturn = 0;
61#line 87
62 setEventCalled = 0;
63#line 88
64 customIrp = 0;
65#line 89
66 return;
67}
68}
69#line 92 "floppy_simpl4.cil.c"
70int PagingReferenceCount = 0;
71#line 93 "floppy_simpl4.cil.c"
72int PagingMutex = 0;
73#line 94 "floppy_simpl4.cil.c"
74int FlAcpiConfigureFloppy(int DisketteExtension , int FdcInfo )
75{
76
77 {
78#line 98
79 return (0);
80}
81}
82#line 101 "floppy_simpl4.cil.c"
83int FlQueueIrpToThread(int Irp , int DisketteExtension )
84{ int status ;
85 int threadHandle = __VERIFIER_nondet_int() ;
86 int DisketteExtension__PoweringDown = __VERIFIER_nondet_int() ;
87 int DisketteExtension__ThreadReferenceCount = __VERIFIER_nondet_int() ;
88 int DisketteExtension__FloppyThread = __VERIFIER_nondet_int() ;
89 int Irp__IoStatus__Status ;
90 int Irp__IoStatus__Information ;
91 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
92 int ObjAttributes = __VERIFIER_nondet_int() ;
93 int __cil_tmp12 ;
94 int __cil_tmp13 ;
95
96 {
97#line 113
98 if (DisketteExtension__PoweringDown == 1) {
99#line 114
100 myStatus = -1073741101;
101#line 115
102 Irp__IoStatus__Status = -1073741101;
103#line 116
104 Irp__IoStatus__Information = 0;
105#line 117
106 return (-1073741101);
107 }
108#line 121
109 DisketteExtension__ThreadReferenceCount ++;
110#line 122
111 if (DisketteExtension__ThreadReferenceCount == 0) {
112#line 123
113 DisketteExtension__ThreadReferenceCount ++;
114#line 124
115 PagingReferenceCount ++;
116#line 125
117 if (PagingReferenceCount == 1) {
118
119 }
120 {
121#line 131
122 status = PsCreateSystemThread(threadHandle, 0, ObjAttributes, 0, 0, FloppyThread,
123 DisketteExtension);
124 }
125 {
126#line 134
127#line 134
128 if (status < 0) {
129#line 135
130 DisketteExtension__ThreadReferenceCount = -1;
131#line 136
132 PagingReferenceCount --;
133#line 137
134 if (PagingReferenceCount == 0) {
135
136 }
137#line 142
138 return (status);
139 }
140 }
141 {
142#line 147
143 status = ObReferenceObjectByHandle(threadHandle, 1048576, 0, KernelMode, DisketteExtension__FloppyThread,
144 0);
145#line 149
146 ZwClose(threadHandle);
147 }
148 {
149#line 151
150#line 151
151 if (status < 0) {
152#line 152
153 return (status);
154 }
155 }
156 }
157#line 159
158
159#line 160
160 if (pended == 0) {
161#line 161
162 pended = 1;
163 } else {
164 {
165#line 164
166 errorFn();
167 }
168 }
169#line 167
170 return (259);
171}
172}
173#line 170 "floppy_simpl4.cil.c"
174int FloppyPnp(int DeviceObject , int Irp )
175{ int DeviceObject__DeviceExtension = __VERIFIER_nondet_int() ;
176 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
177 int Irp__IoStatus__Information ;
178 int Irp__IoStatus__Status ;
179 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
180 int disketteExtension__IsRemoved = __VERIFIER_nondet_int() ;
181 int disketteExtension__IsStarted = __VERIFIER_nondet_int() ;
182 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
183 int disketteExtension__HoldNewRequests ;
184 int disketteExtension__FloppyThread = __VERIFIER_nondet_int() ;
185 int disketteExtension__InterfaceString__Buffer = __VERIFIER_nondet_int() ;
186 int disketteExtension__InterfaceString = __VERIFIER_nondet_int() ;
187 int disketteExtension__ArcName__Length = __VERIFIER_nondet_int() ;
188 int disketteExtension__ArcName = __VERIFIER_nondet_int() ;
189 int irpSp__MinorFunction = __VERIFIER_nondet_int() ;
190 int IoGetConfigurationInformation__FloppyCount = __VERIFIER_nondet_int() ;
191 int irpSp ;
192 int disketteExtension ;
193 int ntStatus ;
194 int doneEvent = __VERIFIER_nondet_int() ;
195 int irpSp___0 ;
196 int nextIrpSp ;
197 int nextIrpSp__Control ;
198 int irpSp___1 ;
199 int irpSp__Context ;
200 int irpSp__Control ;
201 long __cil_tmp29 ;
202 long __cil_tmp30 ;
203
204 {
205#line 199
206 ntStatus = 0;
207#line 200
208 PagingReferenceCount ++;
209#line 201
210 if (PagingReferenceCount == 1) {
211
212 }
213#line 206
214 disketteExtension = DeviceObject__DeviceExtension;
215#line 207
216 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
217#line 208
218 if (disketteExtension__IsRemoved) {
219 {
220#line 210
221 Irp__IoStatus__Information = 0;
222#line 211
223 Irp__IoStatus__Status = -1073741738;
224#line 212
225 myStatus = -1073741738;
226#line 213
227 IofCompleteRequest(Irp, 0);
228 }
229#line 215
230 return (-1073741738);
231 }
232#line 219
233 if (irpSp__MinorFunction == 0) {
234 goto switch_0_0;
235 } else {
236#line 222
237 if (irpSp__MinorFunction == 5) {
238 goto switch_0_5;
239 } else {
240#line 225
241 if (irpSp__MinorFunction == 1) {
242 goto switch_0_5;
243 } else {
244#line 228
245 if (irpSp__MinorFunction == 6) {
246 goto switch_0_6;
247 } else {
248#line 231
249 if (irpSp__MinorFunction == 3) {
250 goto switch_0_6;
251 } else {
252#line 234
253 if (irpSp__MinorFunction == 4) {
254 goto switch_0_4;
255 } else {
256#line 237
257 if (irpSp__MinorFunction == 2) {
258 goto switch_0_2;
259 } else {
260 goto switch_0_default;
261#line 242
262 if (0) {
263 switch_0_0:
264 {
265#line 245
266 ntStatus = FloppyStartDevice(DeviceObject, Irp);
267 }
268 goto switch_0_break;
269 switch_0_5:
270#line 250
271 if (irpSp__MinorFunction == 5) {
272
273 }
274#line 255
275 if (! disketteExtension__IsStarted) {
276#line 256
277 if (s == NP) {
278#line 257
279 s = SKIP1;
280 } else {
281 {
282#line 260
283 errorFn();
284 }
285 }
286 {
287#line 264
288 Irp__CurrentLocation ++;
289#line 265
290 Irp__Tail__Overlay__CurrentStackLocation ++;
291#line 266
292 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
293 }
294#line 268
295 return (ntStatus);
296 }
297 {
298#line 273
299 disketteExtension__HoldNewRequests = 1;
300#line 274
301 ntStatus = FlQueueIrpToThread(Irp, disketteExtension);
302 }
303 {
304#line 276
305 __cil_tmp29 = (long )ntStatus;
306#line 276
307 if (__cil_tmp29 == 259L) {
308 {
309#line 278
310 KeWaitForSingleObject(disketteExtension__FloppyThread, Executive,
311 KernelMode, 0, 0);
312 }
313#line 281
314 if (disketteExtension__FloppyThread != 0) {
315
316 }
317#line 286
318 disketteExtension__FloppyThread = 0;
319#line 287
320 Irp__IoStatus__Status = 0;
321#line 288
322 myStatus = 0;
323#line 289
324 if (s == NP) {
325#line 290
326 s = SKIP1;
327 } else {
328 {
329#line 293
330 errorFn();
331 }
332 }
333 {
334#line 297
335 Irp__CurrentLocation ++;
336#line 298
337 Irp__Tail__Overlay__CurrentStackLocation ++;
338#line 299
339 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
340 }
341 } else {
342 {
343#line 303
344 ntStatus = -1073741823;
345#line 304
346 Irp__IoStatus__Status = ntStatus;
347#line 305
348 myStatus = ntStatus;
349#line 306
350 Irp__IoStatus__Information = 0;
351#line 307
352 IofCompleteRequest(Irp, 0);
353 }
354 }
355 }
356 goto switch_0_break;
357 switch_0_6:
358#line 313
359 if (irpSp__MinorFunction == 6) {
360
361 }
362#line 318
363 if (! disketteExtension__IsStarted) {
364#line 319
365 Irp__IoStatus__Status = 0;
366#line 320
367 myStatus = 0;
368#line 321
369 if (s == NP) {
370#line 322
371 s = SKIP1;
372 } else {
373 {
374#line 325
375 errorFn();
376 }
377 }
378 {
379#line 329
380 Irp__CurrentLocation ++;
381#line 330
382 Irp__Tail__Overlay__CurrentStackLocation ++;
383#line 331
384 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
385 }
386 } else {
387#line 334
388 Irp__IoStatus__Status = 0;
389#line 335
390 myStatus = 0;
391#line 336
392 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
393#line 337
394 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
395#line 338
396 nextIrpSp__Control = 0;
397#line 339
398 if (s != NP) {
399 {
400#line 341
401 errorFn();
402 }
403 } else {
404#line 344
405 if (compRegistered != 0) {
406 {
407#line 346
408 errorFn();
409 }
410 } else {
411#line 349
412 compRegistered = 1;
413 }
414 }
415 {
416#line 353
417 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
418#line 354
419 irpSp__Context = doneEvent;
420#line 355
421 irpSp__Control = 224;
422#line 359
423 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
424 }
425 {
426#line 361
427 __cil_tmp30 = (long )ntStatus;
428#line 361
429 if (__cil_tmp30 == 259L) {
430 {
431#line 363
432 KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
433#line 364
434 ntStatus = myStatus;
435 }
436 }
437 }
438 {
439#line 370
440 disketteExtension__HoldNewRequests = 0;
441#line 371
442 Irp__IoStatus__Status = ntStatus;
443#line 372
444 myStatus = ntStatus;
445#line 373
446 Irp__IoStatus__Information = 0;
447#line 374
448 IofCompleteRequest(Irp, 0);
449 }
450 }
451 goto switch_0_break;
452 switch_0_4:
453#line 379
454 disketteExtension__IsStarted = 0;
455#line 380
456 Irp__IoStatus__Status = 0;
457#line 381
458 myStatus = 0;
459#line 382
460 if (s == NP) {
461#line 383
462 s = SKIP1;
463 } else {
464 {
465#line 386
466 errorFn();
467 }
468 }
469 {
470#line 390
471 Irp__CurrentLocation ++;
472#line 391
473 Irp__Tail__Overlay__CurrentStackLocation ++;
474#line 392
475 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
476 }
477 goto switch_0_break;
478 switch_0_2:
479#line 396
480 disketteExtension__HoldNewRequests = 0;
481#line 397
482 disketteExtension__IsStarted = 0;
483#line 398
484 disketteExtension__IsRemoved = 1;
485#line 399
486 if (s == NP) {
487#line 400
488 s = SKIP1;
489 } else {
490 {
491#line 403
492 errorFn();
493 }
494 }
495 {
496#line 407
497 Irp__CurrentLocation ++;
498#line 408
499 Irp__Tail__Overlay__CurrentStackLocation ++;
500#line 409
501 Irp__IoStatus__Status = 0;
502#line 410
503 myStatus = 0;
504#line 411
505 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
506 }
507#line 413
508 if (disketteExtension__InterfaceString__Buffer != 0) {
509 {
510#line 415
511 IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
512 0);
513 }
514 }
515#line 421
516 if (disketteExtension__ArcName__Length != 0) {
517 {
518#line 423
519 IoDeleteSymbolicLink(disketteExtension__ArcName);
520 }
521 }
522#line 428
523 IoGetConfigurationInformation__FloppyCount --;
524 goto switch_0_break;
525 switch_0_default: ;
526#line 431
527 if (s == NP) {
528#line 432
529 s = SKIP1;
530 } else {
531 {
532#line 435
533 errorFn();
534 }
535 }
536 {
537#line 439
538 Irp__CurrentLocation ++;
539#line 440
540 Irp__Tail__Overlay__CurrentStackLocation ++;
541#line 441
542 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
543 }
544 } else {
545 switch_0_break: ;
546 }
547 }
548 }
549 }
550 }
551 }
552 }
553 }
554#line 454
555 PagingReferenceCount --;
556#line 455
557 if (PagingReferenceCount == 0) {
558
559 }
560#line 460
561 return (ntStatus);
562}
563}
564#line 463 "floppy_simpl4.cil.c"
565int FloppyStartDevice(int DeviceObject , int Irp )
566{ int DeviceObject__DeviceExtension = __VERIFIER_nondet_int() ;
567 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
568 int Irp__IoStatus__Status ;
569 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
570 int disketteExtension__MaxTransferSize ;
571 int disketteExtension__DriveType = __VERIFIER_nondet_int() ;
572 int disketteExtension__PerpendicularMode ;
573 int disketteExtension__DeviceUnit ;
574 int disketteExtension__DriveOnValue ;
575 int disketteExtension__UnderlyingPDO = __VERIFIER_nondet_int() ;
576 int disketteExtension__InterfaceString = __VERIFIER_nondet_int() ;
577 int disketteExtension__IsStarted ;
578 int disketteExtension__HoldNewRequests ;
579 int ntStatus ;
580 int pnpStatus ;
581 int doneEvent = __VERIFIER_nondet_int() ;
582 int fdcInfo = __VERIFIER_nondet_int() ;
583 int fdcInfo__BufferCount ;
584 int fdcInfo__BufferSize ;
585 int fdcInfo__MaxTransferSize = __VERIFIER_nondet_int() ;
586 int fdcInfo__AcpiBios = __VERIFIER_nondet_int() ;
587 int fdcInfo__AcpiFdiSupported = __VERIFIER_nondet_int() ;
588 int fdcInfo__PeripheralNumber = __VERIFIER_nondet_int() ;
589 int fdcInfo__BusType ;
590 int fdcInfo__ControllerNumber = __VERIFIER_nondet_int() ;
591 int fdcInfo__UnitNumber = __VERIFIER_nondet_int() ;
592 int fdcInfo__BusNumber = __VERIFIER_nondet_int() ;
593 int Dc ;
594 int Fp ;
595 int disketteExtension ;
596 int irpSp ;
597 int irpSp___0 ;
598 int nextIrpSp ;
599 int nextIrpSp__Control ;
600 int irpSp___1 ;
601 int irpSp__Control ;
602 int irpSp__Context ;
603 int InterfaceType ;
604 int KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 = __VERIFIER_nondet_int() ;
605 long __cil_tmp42 ;
606 int __cil_tmp43 ;
607 int __cil_tmp44 ;
608 int __cil_tmp45 ;
609 int __cil_tmp46 = __VERIFIER_nondet_int() ;
610 int __cil_tmp47 ;
611 int __cil_tmp48 ;
612 int __cil_tmp49 ;
613
614 {
615#line 505
616 Dc = DiskController;
617#line 506
618 Fp = FloppyDiskPeripheral;
619#line 507
620 disketteExtension = DeviceObject__DeviceExtension;
621#line 508
622 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
623#line 509
624 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
625#line 510
626 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
627#line 511
628 nextIrpSp__Control = 0;
629#line 512
630 if (s != NP) {
631 {
632#line 514
633 errorFn();
634 }
635 } else {
636#line 517
637 if (compRegistered != 0) {
638 {
639#line 519
640 errorFn();
641 }
642 } else {
643#line 522
644 compRegistered = 1;
645 }
646 }
647 {
648#line 526
649 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
650#line 527
651 irpSp__Context = doneEvent;
652#line 528
653 irpSp__Control = 224;
654#line 532
655 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
656 }
657 {
658#line 534
659 __cil_tmp42 = (long )ntStatus;
660#line 534
661 if (__cil_tmp42 == 259L) {
662 {
663#line 536
664 ntStatus = KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
665#line 537
666 ntStatus = myStatus;
667 }
668 }
669 }
670 {
671#line 543
672 fdcInfo__BufferCount = 0;
673#line 544
674 fdcInfo__BufferSize = 0;
675#line 545
676
677#line 545
678
679#line 545
680
681#line 545
682
683#line 545
684 ntStatus = FlFdcDeviceIo(disketteExtension__TargetObject, __cil_tmp46, fdcInfo);
685 }
686#line 548
687 if (ntStatus >= 0) {
688#line 549
689 disketteExtension__MaxTransferSize = fdcInfo__MaxTransferSize;
690#line 550
691 if (fdcInfo__AcpiBios) {
692#line 551
693 if (fdcInfo__AcpiFdiSupported) {
694 {
695#line 553
696 ntStatus = FlAcpiConfigureFloppy(disketteExtension, fdcInfo);
697 }
698#line 555
699 if (disketteExtension__DriveType == 4) {
700#line 556
701
702#line 556
703
704 }
705 } else {
706 goto _L;
707 }
708 } else {
709 _L:
710#line 565
711 if (disketteExtension__DriveType == 4) {
712#line 566
713
714#line 566
715
716 }
717#line 570
718 InterfaceType = 0;
719 {
720#line 572
721 while (1) {
722 while_0_continue: ;
723
724#line 574
725 if (InterfaceType >= MaximumInterfaceType) {
726 goto while_1_break;
727 }
728 {
729#line 580
730 fdcInfo__BusType = InterfaceType;
731#line 581
732 ntStatus = IoQueryDeviceDescription(fdcInfo__BusType, fdcInfo__BusNumber,
733 Dc, fdcInfo__ControllerNumber, Fp, fdcInfo__PeripheralNumber,
734 FlConfigCallBack, disketteExtension);
735 }
736#line 585
737 if (ntStatus >= 0) {
738 goto while_1_break;
739 }
740#line 590
741 InterfaceType ++;
742 }
743 while_0_break: ;
744 }
745 while_1_break: ;
746 }
747#line 595
748 if (ntStatus >= 0) {
749#line 596
750 if (KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 != 0) {
751#line 597
752 disketteExtension__DeviceUnit = fdcInfo__UnitNumber;
753#line 598
754 disketteExtension__DriveOnValue = fdcInfo__UnitNumber;
755 } else {
756#line 600
757 disketteExtension__DeviceUnit = fdcInfo__PeripheralNumber;
758#line 601
759
760#line 601
761
762 }
763 {
764#line 604
765 pnpStatus = IoRegisterDeviceInterface(disketteExtension__UnderlyingPDO, MOUNTDEV_MOUNTED_DEVICE_GUID,
766 0, disketteExtension__InterfaceString);
767 }
768#line 607
769 if (pnpStatus >= 0) {
770 {
771#line 609
772 pnpStatus = IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
773 1);
774 }
775 }
776#line 615
777 disketteExtension__IsStarted = 1;
778#line 616
779 disketteExtension__HoldNewRequests = 0;
780 }
781 }
782 {
783#line 624
784 Irp__IoStatus__Status = ntStatus;
785#line 625
786 myStatus = ntStatus;
787#line 626
788 IofCompleteRequest(Irp, 0);
789 }
790#line 628
791 return (ntStatus);
792}
793}
794#line 631 "floppy_simpl4.cil.c"
795int FloppyPnpComplete(int DeviceObject , int Irp , int Context )
796{
797
798 {
799 {
800#line 636
801 KeSetEvent(Context, 1, 0);
802 }
803#line 638
804 return (-1073741802);
805}
806}
807#line 641 "floppy_simpl4.cil.c"
808int FlFdcDeviceIo(int DeviceObject , int Ioctl , int Data )
809{ int ntStatus ;
810 int irp ;
811 int irpStack ;
812 int doneEvent = __VERIFIER_nondet_int() ;
813 int ioStatus = __VERIFIER_nondet_int() ;
814 int irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
815 int irpStack__Parameters__DeviceIoControl__Type3InputBuffer ;
816 long __cil_tmp11 ;
817
818 {
819 {
820#line 652
821 irp = IoBuildDeviceIoControlRequest(Ioctl, DeviceObject, 0, 0, 0, 0, 1, doneEvent,
822 ioStatus);
823 }
824#line 655
825 if (irp == 0) {
826#line 656
827 return (-1073741670);
828 }
829 {
830#line 661
831 irpStack = irp__Tail__Overlay__CurrentStackLocation - 1;
832#line 662
833 irpStack__Parameters__DeviceIoControl__Type3InputBuffer = Data;
834#line 663
835 ntStatus = IofCallDriver(DeviceObject, irp);
836 }
837 {
838#line 665
839 __cil_tmp11 = (long )ntStatus;
840#line 665
841 if (__cil_tmp11 == 259L) {
842 {
843#line 667
844 KeWaitForSingleObject(doneEvent, Suspended, KernelMode, 0, 0);
845#line 668
846 ntStatus = myStatus;
847 }
848 }
849 }
850#line 673
851 return (ntStatus);
852}
853}
854#line 676 "floppy_simpl4.cil.c"
855void FloppyProcessQueuedRequests(int DisketteExtension )
856{
857
858 {
859#line 680
860 return;
861}
862}
863#line 683 "floppy_simpl4.cil.c"
864void stub_driver_init(void)
865{
866
867 {
868#line 687
869 s = NP;
870#line 688
871 pended = 0;
872#line 689
873 compRegistered = 0;
874#line 690
875 lowerDriverReturn = 0;
876#line 691
877 setEventCalled = 0;
878#line 692
879 customIrp = 0;
880#line 693
881 return;
882}
883}
884#line 696 "floppy_simpl4.cil.c"
885int main(void)
886{ int status ;
887 int irp = __VERIFIER_nondet_int() ;
888 int pirp ;
889 int pirp__IoStatus__Status ;
890 int irp_choice = __VERIFIER_nondet_int() ;
891 int devobj = __VERIFIER_nondet_int() ;
892 int __cil_tmp8 ;
893
894 FloppyThread = 0;
895 KernelMode = 0;
896 Suspended = 0;
897 Executive = 0;
898 DiskController = 0;
899 FloppyDiskPeripheral = 0;
900 FlConfigCallBack = 0;
901 MaximumInterfaceType = 0;
902 MOUNTDEV_MOUNTED_DEVICE_GUID = 0;
903 myStatus = 0;
904 s = 0;
905 UNLOADED = 0;
906 NP = 0;
907 DC = 0;
908 SKIP1 = 0;
909 SKIP2 = 0 ;
910 MPR1 = 0;
911 MPR3 = 0;
912 IPC = 0;
913 pended = 0;
914 compRegistered = 0;
915 lowerDriverReturn = 0;
916 setEventCalled = 0;
917 customIrp = 0;
918
919 {
920 {
921#line 707
922 status = 0;
923#line 708
924 pirp = irp;
925#line 709
926 _BLAST_init();
927 }
928#line 711
929 if (status >= 0) {
930#line 712
931 s = NP;
932#line 713
933 customIrp = 0;
934#line 714
935 setEventCalled = customIrp;
936#line 715
937 lowerDriverReturn = setEventCalled;
938#line 716
939 compRegistered = lowerDriverReturn;
940#line 717
941 pended = compRegistered;
942#line 718
943 pirp__IoStatus__Status = 0;
944#line 719
945 myStatus = 0;
946#line 720
947 if (irp_choice == 0) {
948#line 721
949 pirp__IoStatus__Status = -1073741637;
950#line 722
951 myStatus = -1073741637;
952 }
953 {
954#line 727
955 stub_driver_init();
956 }
957 {
958#line 729
959#line 729
960 if (status < 0) {
961#line 730
962 return (-1);
963 }
964 }
965#line 734
966 int tmp_ndt_1;
967 tmp_ndt_1 = __VERIFIER_nondet_int();
968 if (tmp_ndt_1 == 0) {
969 goto switch_2_0;
970 } else {
971#line 737
972 int tmp_ndt_2;
973 tmp_ndt_2 = __VERIFIER_nondet_int();
974 if (tmp_ndt_2 == 1) {
975 goto switch_2_1;
976 } else {
977#line 740
978 int tmp_ndt_3;
979 tmp_ndt_3 = __VERIFIER_nondet_int();
980 if (tmp_ndt_3 == 2) {
981 goto switch_2_2;
982 } else {
983#line 743
984 int tmp_ndt_4;
985 tmp_ndt_4 = __VERIFIER_nondet_int();
986 if (tmp_ndt_4 == 3) {
987 goto switch_2_3;
988 } else {
989 goto switch_2_default;
990#line 748
991 if (0) {
992 switch_2_0:
993 {
994#line 751
995 status = FloppyCreateClose(devobj, pirp);
996 }
997 goto switch_2_break;
998 switch_2_1:
999 {
1000#line 756
1001 status = FloppyCreateClose(devobj, pirp);
1002 }
1003 goto switch_2_break;
1004 switch_2_2:
1005 {
1006#line 761
1007 status = FloppyDeviceControl(devobj, pirp);
1008 }
1009 goto switch_2_break;
1010 switch_2_3:
1011 {
1012#line 766
1013 status = FloppyPnp(devobj, pirp);
1014 }
1015 goto switch_2_break;
1016 switch_2_default: ;
1017#line 770
1018 return (-1);
1019 } else {
1020 switch_2_break: ;
1021 }
1022 }
1023 }
1024 }
1025 }
1026 }
1027#line 782
1028 if (pended == 1) {
1029#line 783
1030 if (s == NP) {
1031#line 784
1032 s = NP;
1033 } else {
1034 goto _L___2;
1035 }
1036 } else {
1037 _L___2:
1038#line 790
1039 if (pended == 1) {
1040#line 791
1041 if (s == MPR3) {
1042#line 792
1043 s = MPR3;
1044 } else {
1045 goto _L___1;
1046 }
1047 } else {
1048 _L___1:
1049#line 798
1050 if (s != UNLOADED) {
1051#line 801
1052 if (status != -1) {
1053#line 804
1054 if (s != SKIP2) {
1055#line 805
1056 if (s != IPC) {
1057#line 806
1058 if (s != DC) {
1059 {
1060#line 808
1061 errorFn();
1062 }
1063 } else {
1064 goto _L___0;
1065 }
1066 } else {
1067 goto _L___0;
1068 }
1069 } else {
1070 _L___0:
1071#line 818
1072 if (pended == 1) {
1073#line 819
1074 if (status != 259) {
1075#line 820
1076 status = 0;
1077 }
1078 } else {
1079#line 825
1080 if (s == DC) {
1081#line 826
1082 if (status == 259) {
1083 {
1084#line 828
1085 errorFn();
1086 }
1087 }
1088 } else {
1089#line 834
1090 if (status != lowerDriverReturn) {
1091 {
1092#line 836
1093 errorFn();
1094 }
1095 }
1096 }
1097 }
1098 }
1099 }
1100 }
1101 }
1102 }
1103#line 848
1104 status = 0;
1105#line 849
1106 return (status);
1107}
1108}
1109#line 852 "floppy_simpl4.cil.c"
1110int IoBuildDeviceIoControlRequest(int IoControlCode , int DeviceObject , int InputBuffer ,
1111 int InputBufferLength , int OutputBuffer , int OutputBufferLength ,
1112 int InternalDeviceIoControl , int Event , int IoStatusBlock )
1113{
1114 int malloc = __VERIFIER_nondet_int() ;
1115
1116 {
1117#line 859
1118 customIrp = 1;
1119#line 860
1120 int tmp_ndt_5;
1121 tmp_ndt_5 = __VERIFIER_nondet_int();
1122 if (tmp_ndt_5 == 0) {
1123 goto switch_3_0;
1124 } else {
1125 goto switch_3_default;
1126#line 865
1127 if (0) {
1128 switch_3_0:
1129#line 867
1130 return (malloc);
1131 switch_3_default: ;
1132#line 869
1133 return (0);
1134 } else {
1135
1136 }
1137 }
1138}
1139}
1140#line 877 "floppy_simpl4.cil.c"
1141int IoDeleteSymbolicLink(int SymbolicLinkName )
1142{
1143
1144 {
1145#line 881
1146 int tmp_ndt_6;
1147 tmp_ndt_6 = __VERIFIER_nondet_int();
1148 if (tmp_ndt_6 == 0) {
1149 goto switch_4_0;
1150 } else {
1151 goto switch_4_default;
1152#line 886
1153 if (0) {
1154 switch_4_0:
1155#line 888
1156 return (0);
1157 switch_4_default: ;
1158#line 890
1159 return (-1073741823);
1160 } else {
1161
1162 }
1163 }
1164}
1165}
1166#line 898 "floppy_simpl4.cil.c"
1167int IoQueryDeviceDescription(int BusType , int BusNumber , int ControllerType , int ControllerNumber ,
1168 int PeripheralType , int PeripheralNumber , int CalloutRoutine ,
1169 int Context )
1170{
1171
1172 {
1173#line 904
1174 int tmp_ndt_7;
1175 tmp_ndt_7 = __VERIFIER_nondet_int();
1176 if (tmp_ndt_7 == 0) {
1177 goto switch_5_0;
1178 } else {
1179 goto switch_5_default;
1180#line 909
1181 if (0) {
1182 switch_5_0:
1183#line 911
1184 return (0);
1185 switch_5_default: ;
1186#line 913
1187 return (-1073741823);
1188 } else {
1189
1190 }
1191 }
1192}
1193}
1194#line 921 "floppy_simpl4.cil.c"
1195int IoRegisterDeviceInterface(int PhysicalDeviceObject , int InterfaceClassGuid ,
1196 int ReferenceString , int SymbolicLinkName )
1197{
1198
1199 {
1200#line 926
1201 int tmp_ndt_8;
1202 tmp_ndt_8 = __VERIFIER_nondet_int();
1203 if (tmp_ndt_8 == 0) {
1204 goto switch_6_0;
1205 } else {
1206 goto switch_6_default;
1207#line 931
1208 if (0) {
1209 switch_6_0:
1210#line 933
1211 return (0);
1212 switch_6_default: ;
1213#line 935
1214 return (-1073741808);
1215 } else {
1216
1217 }
1218 }
1219}
1220}
1221#line 943 "floppy_simpl4.cil.c"
1222int IoSetDeviceInterfaceState(int SymbolicLinkName , int Enable )
1223{
1224
1225 {
1226#line 947
1227 int tmp_ndt_9;
1228 tmp_ndt_9 = __VERIFIER_nondet_int();
1229 if (tmp_ndt_9 == 0) {
1230 goto switch_7_0;
1231 } else {
1232 goto switch_7_default;
1233#line 952
1234 if (0) {
1235 switch_7_0:
1236#line 954
1237 return (0);
1238 switch_7_default: ;
1239#line 956
1240 return (-1073741823);
1241 } else {
1242
1243 }
1244 }
1245}
1246}
1247#line 964 "floppy_simpl4.cil.c"
1248void stubMoreProcessingRequired(void)
1249{
1250
1251 {
1252#line 968
1253 if (s == NP) {
1254#line 969
1255 s = MPR1;
1256 } else {
1257 {
1258#line 972
1259 errorFn();
1260 }
1261 }
1262#line 975
1263 return;
1264}
1265}
1266#line 978 "floppy_simpl4.cil.c"
1267int IofCallDriver(int DeviceObject , int Irp )
1268{
1269 int returnVal2 ;
1270 int compRetStatus1 ;
1271 int lcontext = __VERIFIER_nondet_int() ;
1272 unsigned long __cil_tmp7 ;
1273
1274 {
1275#line 985
1276 if (compRegistered) {
1277 {
1278#line 987
1279 compRetStatus1 = FloppyPnpComplete(DeviceObject, Irp, lcontext);
1280 }
1281 {
1282#line 989
1283 __cil_tmp7 = (unsigned long )compRetStatus1;
1284#line 989
1285 if (__cil_tmp7 == -1073741802) {
1286 {
1287#line 991
1288 stubMoreProcessingRequired();
1289 }
1290 }
1291 }
1292 }
1293#line 999
1294 int tmp_ndt_10;
1295 tmp_ndt_10 = __VERIFIER_nondet_int();
1296 if (tmp_ndt_10 == 0) {
1297 goto switch_8_0;
1298 } else {
1299#line 1002
1300 int tmp_ndt_11;
1301 tmp_ndt_11 = __VERIFIER_nondet_int();
1302 if (tmp_ndt_11 == 1) {
1303 goto switch_8_1;
1304 } else {
1305 goto switch_8_default;
1306#line 1007
1307 if (0) {
1308 switch_8_0:
1309#line 1009
1310 returnVal2 = 0;
1311 goto switch_8_break;
1312 switch_8_1:
1313#line 1012
1314 returnVal2 = -1073741823;
1315 goto switch_8_break;
1316 switch_8_default:
1317#line 1015
1318 returnVal2 = 259;
1319 goto switch_8_break;
1320 } else {
1321 switch_8_break: ;
1322 }
1323 }
1324 }
1325#line 1023
1326 if (s == NP) {
1327#line 1024
1328 s = IPC;
1329#line 1025
1330 lowerDriverReturn = returnVal2;
1331 } else {
1332#line 1027
1333 if (s == MPR1) {
1334#line 1028
1335 if (returnVal2 == 259) {
1336#line 1029
1337 s = MPR3;
1338#line 1030
1339 lowerDriverReturn = returnVal2;
1340 } else {
1341#line 1032
1342 s = NP;
1343#line 1033
1344 lowerDriverReturn = returnVal2;
1345 }
1346 } else {
1347#line 1036
1348 if (s == SKIP1) {
1349#line 1037
1350 s = SKIP2;
1351#line 1038
1352 lowerDriverReturn = returnVal2;
1353 } else {
1354 {
1355#line 1041
1356 errorFn();
1357 }
1358 }
1359 }
1360 }
1361#line 1046
1362 return (returnVal2);
1363}
1364}
1365#line 1049 "floppy_simpl4.cil.c"
1366void IofCompleteRequest(int Irp , int PriorityBoost )
1367{
1368
1369 {
1370#line 1053
1371 if (s == NP) {
1372#line 1054
1373 s = DC;
1374 } else {
1375 {
1376#line 1057
1377 errorFn();
1378 }
1379 }
1380#line 1060
1381 return;
1382}
1383}
1384#line 1063 "floppy_simpl4.cil.c"
1385int KeSetEvent(int Event , int Increment , int Wait )
1386{ int l = __VERIFIER_nondet_int() ;
1387
1388 {
1389#line 1067
1390 setEventCalled = 1;
1391#line 1068
1392 return (l);
1393}
1394}
1395#line 1071 "floppy_simpl4.cil.c"
1396int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
1397 int Timeout )
1398{
1399
1400 {
1401#line 1076
1402 if (s == MPR3) {
1403#line 1077
1404 if (setEventCalled == 1) {
1405#line 1078
1406 s = NP;
1407#line 1079
1408 setEventCalled = 0;
1409 } else {
1410 goto _L;
1411 }
1412 } else {
1413 _L:
1414#line 1085
1415 if (customIrp == 1) {
1416#line 1086
1417 s = NP;
1418#line 1087
1419 customIrp = 0;
1420 } else {
1421#line 1089
1422 if (s == MPR3) {
1423 {
1424#line 1091
1425 errorFn();
1426 }
1427 }
1428 }
1429 }
1430#line 1098
1431 int tmp_ndt_12;
1432 tmp_ndt_12 = __VERIFIER_nondet_int();
1433 if (tmp_ndt_12 == 0) {
1434 goto switch_9_0;
1435 } else {
1436 goto switch_9_default;
1437#line 1103
1438 if (0) {
1439 switch_9_0:
1440#line 1105
1441 return (0);
1442 switch_9_default: ;
1443#line 1107
1444 return (-1073741823);
1445 } else {
1446
1447 }
1448 }
1449}
1450}
1451#line 1115 "floppy_simpl4.cil.c"
1452int ObReferenceObjectByHandle(int Handle , int DesiredAccess , int ObjectType , int AccessMode ,
1453 int Object , int HandleInformation )
1454{
1455
1456 {
1457#line 1120
1458 int tmp_ndt_13;
1459 tmp_ndt_13 = __VERIFIER_nondet_int();
1460 if (tmp_ndt_13 == 0) {
1461 goto switch_10_0;
1462 } else {
1463 goto switch_10_default;
1464#line 1125
1465 if (0) {
1466 switch_10_0:
1467#line 1127
1468 return (0);
1469 switch_10_default: ;
1470#line 1129
1471 return (-1073741823);
1472 } else {
1473
1474 }
1475 }
1476}
1477}
1478#line 1137 "floppy_simpl4.cil.c"
1479int PsCreateSystemThread(int ThreadHandle , int DesiredAccess , int ObjectAttributes ,
1480 int ProcessHandle , int ClientId , int StartRoutine , int StartContext )
1481{
1482
1483 {
1484#line 1142
1485 int tmp_ndt_14;
1486 tmp_ndt_14 = __VERIFIER_nondet_int();
1487 if (tmp_ndt_14 == 0) {
1488 goto switch_11_0;
1489 } else {
1490 goto switch_11_default;
1491#line 1147
1492 if (0) {
1493 switch_11_0:
1494#line 1149
1495 return (0);
1496 switch_11_default: ;
1497#line 1151
1498 return (-1073741823);
1499 } else {
1500
1501 }
1502 }
1503}
1504}
1505#line 1159 "floppy_simpl4.cil.c"
1506int ZwClose(int Handle )
1507{
1508
1509 {
1510#line 1163
1511 int tmp_ndt_15;
1512 tmp_ndt_15 = __VERIFIER_nondet_int();
1513 if (tmp_ndt_15 == 0) {
1514 goto switch_12_0;
1515 } else {
1516 goto switch_12_default;
1517#line 1168
1518 if (0) {
1519 switch_12_0:
1520#line 1170
1521 return (0);
1522 switch_12_default: ;
1523#line 1172
1524 return (-1073741823);
1525 } else {
1526
1527 }
1528 }
1529}
1530}
1531#line 1180 "floppy_simpl4.cil.c"
1532int FloppyCreateClose(int DeviceObject , int Irp )
1533{ int Irp__IoStatus__Status ;
1534 int Irp__IoStatus__Information ;
1535
1536 {
1537 {
1538#line 1186
1539 myStatus = 0;
1540#line 1187
1541 Irp__IoStatus__Status = 0;
1542#line 1188
1543 Irp__IoStatus__Information = 1;
1544#line 1189
1545 IofCompleteRequest(Irp, 0);
1546 }
1547#line 1191
1548 return (0);
1549}
1550}
1551#line 1194
1552int FloppyQueueRequest(int DisketteExtension , int Irp ) ;
1553#line 1195 "floppy_simpl4.cil.c"
1554int FloppyDeviceControl(int DeviceObject , int Irp )
1555{ int disketteExtension__HoldNewRequests = __VERIFIER_nondet_int() ;
1556 int disketteExtension__IsRemoved = __VERIFIER_nondet_int() ;
1557 int Irp__IoStatus__Information ;
1558 int disketteExtension__IsStarted = __VERIFIER_nondet_int() ;
1559 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
1560 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
1561 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
1562 int irpSp__Parameters__DeviceIoControl__OutputBufferLength = __VERIFIER_nondet_int() ;
1563 int sizeof__MOUNTDEV_NAME = __VERIFIER_nondet_int() ;
1564 int Irp__AssociatedIrp__SystemBuffer = __VERIFIER_nondet_int() ;
1565 int mountName__NameLength ;
1566 int disketteExtension__DeviceName__Length = __VERIFIER_nondet_int() ;
1567 int sizeof__USHORT = __VERIFIER_nondet_int() ;
1568 int disketteExtension__InterfaceString__Buffer = __VERIFIER_nondet_int() ;
1569 int uniqueId__UniqueIdLength ;
1570 int disketteExtension__InterfaceString__Length = __VERIFIER_nondet_int() ;
1571 int sizeof__MOUNTDEV_UNIQUE_ID = __VERIFIER_nondet_int() ;
1572 int irpSp__Parameters__DeviceIoControl__InputBufferLength = __VERIFIER_nondet_int() ;
1573 int sizeof__FORMAT_PARAMETERS = __VERIFIER_nondet_int() ;
1574 int irpSp__Parameters__DeviceIoControl__IoControlCode___1 = __VERIFIER_nondet_int() ;
1575 int sizeof__FORMAT_EX_PARAMETERS = __VERIFIER_nondet_int() ;
1576 int formatExParameters__FormatGapLength = __VERIFIER_nondet_int() ;
1577 int formatExParameters__SectorsPerTrack = __VERIFIER_nondet_int() ;
1578 int sizeof__DISK_GEOMETRY = __VERIFIER_nondet_int() ;
1579 int Irp__IoStatus__Status___0 ;
1580 int disketteExtension = __VERIFIER_nondet_int() ;
1581 int ntStatus ;
1582 int outputBufferLength ;
1583 int lowestDriveMediaType = __VERIFIER_nondet_int() ;
1584 int highestDriveMediaType = __VERIFIER_nondet_int() ;
1585 int formatExParametersSize = __VERIFIER_nondet_int() ;
1586 int formatExParameters ;
1587 int tmp ;
1588 int mountName ;
1589 int uniqueId ;
1590 int tmp___0 ;
1591 int __cil_tmp39 ;
1592 int __cil_tmp40 ;
1593 int __cil_tmp41 = __VERIFIER_nondet_int() ;
1594 int __cil_tmp42 ;
1595 int __cil_tmp43 ;
1596 int __cil_tmp44 = __VERIFIER_nondet_int() ;
1597 int __cil_tmp45 = __VERIFIER_nondet_int() ;
1598 int __cil_tmp46 ;
1599 int __cil_tmp47 ;
1600 int __cil_tmp48 ;
1601 int __cil_tmp49 ;
1602 int __cil_tmp50 = __VERIFIER_nondet_int() ;
1603 int __cil_tmp51 ;
1604 int __cil_tmp52 ;
1605 int __cil_tmp53 ;
1606 int __cil_tmp54 ;
1607 int __cil_tmp55 = __VERIFIER_nondet_int() ;
1608 int __cil_tmp56 ;
1609 int __cil_tmp57 ;
1610 int __cil_tmp58 ;
1611 int __cil_tmp59 ;
1612 int __cil_tmp60 = __VERIFIER_nondet_int() ;
1613 int __cil_tmp61 ;
1614 int __cil_tmp62 ;
1615 int __cil_tmp63 ;
1616 int __cil_tmp64 ;
1617 int __cil_tmp65 = __VERIFIER_nondet_int() ;
1618 int __cil_tmp66 = __VERIFIER_nondet_int() ;
1619 int __cil_tmp67 ;
1620 int __cil_tmp68 ;
1621 int __cil_tmp69 = __VERIFIER_nondet_int() ;
1622 int __cil_tmp70 ;
1623 int __cil_tmp71 ;
1624 int __cil_tmp72 = __VERIFIER_nondet_int() ;
1625 int __cil_tmp73 ;
1626 int __cil_tmp74 ;
1627 int __cil_tmp75 = __VERIFIER_nondet_int() ;
1628 int __cil_tmp76 ;
1629 int __cil_tmp77 ;
1630 int __cil_tmp78 = __VERIFIER_nondet_int() ;
1631 int __cil_tmp79 ;
1632 int __cil_tmp80 ;
1633 int __cil_tmp81 = __VERIFIER_nondet_int() ;
1634 int __cil_tmp82 ;
1635 int __cil_tmp83 ;
1636 int __cil_tmp84 ;
1637 int __cil_tmp85 ;
1638 int __cil_tmp86 ;
1639 int __cil_tmp87 ;
1640 int __cil_tmp88 = __VERIFIER_nondet_int() ;
1641 int __cil_tmp89 ;
1642 int __cil_tmp90 ;
1643 long __cil_tmp91 ;
1644
1645 {
1646#line 1234
1647 if (disketteExtension__HoldNewRequests) {
1648 {
1649#line 1235
1650
1651#line 1235
1652
1653#line 1235
1654
1655#line 1235
1656 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 != __cil_tmp41) {
1657 {
1658#line 1237
1659 ntStatus = FloppyQueueRequest(disketteExtension, Irp);
1660 }
1661#line 1239
1662 return (ntStatus);
1663 }
1664 }
1665 }
1666#line 1246
1667 if (disketteExtension__IsRemoved) {
1668 {
1669#line 1248
1670 Irp__IoStatus__Information = 0;
1671#line 1249
1672 Irp__IoStatus__Status___0 = -1073741738;
1673#line 1250
1674 myStatus = -1073741738;
1675#line 1251
1676 IofCompleteRequest(Irp, 0);
1677 }
1678#line 1253
1679 return (-1073741738);
1680 }
1681#line 1257
1682 if (! disketteExtension__IsStarted) {
1683#line 1258
1684 if (s == NP) {
1685#line 1259
1686 s = SKIP1;
1687 } else {
1688 {
1689#line 1262
1690 errorFn();
1691 }
1692 }
1693 {
1694#line 1266
1695 Irp__CurrentLocation ++;
1696#line 1267
1697 Irp__Tail__Overlay__CurrentStackLocation ++;
1698#line 1268
1699 tmp = IofCallDriver(disketteExtension__TargetObject, Irp);
1700 }
1701#line 1270
1702 return (tmp);
1703 }
1704 {
1705#line 1274
1706
1707#line 1274
1708
1709#line 1274
1710
1711#line 1274
1712 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp44) {
1713 goto switch_13_exp_0;
1714 } else {
1715 {
1716#line 1277
1717
1718#line 1277
1719 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp45) {
1720 goto switch_13_exp_1;
1721 } else {
1722 {
1723#line 1280
1724
1725#line 1280
1726
1727#line 1280
1728
1729#line 1280
1730
1731#line 1280
1732
1733#line 1280
1734 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp50) {
1735 goto switch_13_exp_2;
1736 } else {
1737 {
1738#line 1283
1739
1740#line 1283
1741
1742#line 1283
1743
1744#line 1283
1745
1746#line 1283
1747
1748#line 1283
1749 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp55) {
1750 goto switch_13_exp_3;
1751 } else {
1752 {
1753#line 1286
1754
1755#line 1286
1756
1757#line 1286
1758
1759#line 1286
1760
1761#line 1286
1762
1763#line 1286
1764 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp60) {
1765 goto switch_13_exp_4;
1766 } else {
1767 {
1768#line 1289
1769
1770#line 1289
1771
1772#line 1289
1773
1774#line 1289
1775
1776#line 1289
1777
1778#line 1289
1779 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp65) {
1780 goto switch_13_exp_5;
1781 } else {
1782 {
1783#line 1292
1784
1785#line 1292
1786 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp66) {
1787 goto switch_13_exp_6;
1788 } else {
1789 {
1790#line 1295
1791
1792#line 1295
1793
1794#line 1295
1795
1796#line 1295
1797 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp69) {
1798 goto switch_13_exp_7;
1799 } else {
1800 {
1801#line 1298
1802
1803#line 1298
1804
1805#line 1298
1806
1807#line 1298
1808 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp72) {
1809 goto switch_13_exp_8;
1810 } else {
1811 {
1812#line 1301
1813
1814#line 1301
1815
1816#line 1301
1817
1818#line 1301
1819 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp75) {
1820 goto switch_13_exp_9;
1821 } else {
1822 {
1823#line 1304
1824
1825#line 1304
1826
1827#line 1304
1828
1829#line 1304
1830 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp78) {
1831 goto switch_13_exp_10;
1832 } else {
1833 {
1834#line 1307
1835
1836#line 1307
1837
1838#line 1307
1839
1840#line 1307
1841 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp81) {
1842 goto switch_13_exp_11;
1843 } else {
1844 goto switch_13_default;
1845#line 1312
1846 if (0) {
1847 switch_13_exp_0: ;
1848#line 1314
1849 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < sizeof__MOUNTDEV_NAME) {
1850#line 1315
1851 ntStatus = -1073741811;
1852 goto switch_13_break;
1853 }
1854#line 1320
1855 mountName = Irp__AssociatedIrp__SystemBuffer;
1856#line 1321
1857 mountName__NameLength = disketteExtension__DeviceName__Length;
1858 {
1859#line 1322
1860 __cil_tmp82 = sizeof__USHORT + mountName__NameLength;
1861#line 1322
1862 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < __cil_tmp82) {
1863#line 1323
1864 ntStatus = -2147483643;
1865#line 1324
1866 Irp__IoStatus__Information = sizeof__MOUNTDEV_NAME;
1867 goto switch_13_break;
1868 }
1869 }
1870#line 1329
1871 ntStatus = 0;
1872#line 1330
1873 Irp__IoStatus__Information = sizeof__USHORT + mountName__NameLength;
1874 goto switch_13_break;
1875 switch_13_exp_1: ;
1876#line 1333
1877 if (! disketteExtension__InterfaceString__Buffer) {
1878#line 1334
1879 ntStatus = -1073741811;
1880 goto switch_13_break;
1881 } else {
1882#line 1337
1883 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < sizeof__MOUNTDEV_UNIQUE_ID) {
1884#line 1338
1885 ntStatus = -1073741811;
1886 goto switch_13_break;
1887 }
1888 }
1889#line 1344
1890 uniqueId = Irp__AssociatedIrp__SystemBuffer;
1891#line 1345
1892 uniqueId__UniqueIdLength = disketteExtension__InterfaceString__Length;
1893 {
1894#line 1346
1895 __cil_tmp83 = sizeof__USHORT + uniqueId__UniqueIdLength;
1896#line 1346
1897 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < __cil_tmp83) {
1898#line 1347
1899 ntStatus = -2147483643;
1900#line 1348
1901 Irp__IoStatus__Information = sizeof__MOUNTDEV_UNIQUE_ID;
1902 goto switch_13_break;
1903 }
1904 }
1905#line 1353
1906 ntStatus = 0;
1907#line 1354
1908 Irp__IoStatus__Information = sizeof__USHORT + uniqueId__UniqueIdLength;
1909 goto switch_13_break;
1910 switch_13_exp_2: ;
1911 switch_13_exp_3: ;
1912#line 1358
1913 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < sizeof__FORMAT_PARAMETERS) {
1914#line 1359
1915 ntStatus = -1073741811;
1916 goto switch_13_break;
1917 }
1918 {
1919#line 1365
1920 tmp___0 = FlCheckFormatParameters(disketteExtension, Irp__AssociatedIrp__SystemBuffer);
1921 }
1922#line 1367
1923 if (! tmp___0) {
1924#line 1370
1925 ntStatus = -1073741811;
1926 goto switch_13_break;
1927 }
1928 {
1929#line 1373
1930
1931#line 1373
1932
1933#line 1373
1934
1935#line 1373
1936
1937#line 1373
1938
1939#line 1373
1940 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp88) {
1941#line 1374
1942 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < sizeof__FORMAT_EX_PARAMETERS) {
1943#line 1375
1944 ntStatus = -1073741811;
1945 goto switch_13_break;
1946 }
1947#line 1380
1948 formatExParameters = Irp__AssociatedIrp__SystemBuffer;
1949#line 1381
1950 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < formatExParametersSize) {
1951#line 1382
1952 ntStatus = -1073741811;
1953 goto switch_13_break;
1954 } else {
1955#line 1385
1956 if (formatExParameters__FormatGapLength >= 256) {
1957#line 1386
1958 ntStatus = -1073741811;
1959 goto switch_13_break;
1960 } else {
1961#line 1389
1962 if (formatExParameters__SectorsPerTrack >= 256) {
1963#line 1390
1964 ntStatus = -1073741811;
1965 goto switch_13_break;
1966 }
1967 }
1968 }
1969 }
1970 }
1971 switch_13_exp_4: ;
1972 switch_13_exp_5: ;
1973 switch_13_exp_6: ;
1974 switch_13_exp_7:
1975 {
1976#line 1405
1977 ntStatus = FlQueueIrpToThread(Irp, disketteExtension);
1978 }
1979 goto switch_13_break;
1980 switch_13_exp_8: ;
1981 switch_13_exp_9:
1982#line 1410
1983 outputBufferLength = irpSp__Parameters__DeviceIoControl__OutputBufferLength;
1984#line 1411
1985 if (outputBufferLength < sizeof__DISK_GEOMETRY) {
1986#line 1412
1987 ntStatus = -1073741789;
1988 goto switch_13_break;
1989 }
1990#line 1417
1991 ntStatus = 0;
1992 {
1993#line 1418
1994 __cil_tmp89 = highestDriveMediaType - lowestDriveMediaType;
1995#line 1418
1996 __cil_tmp90 = __cil_tmp89 + 1;
1997#line 1418
1998 if (outputBufferLength < __cil_tmp90) {
1999#line 1419
2000 ntStatus = -2147483643;
2001 }
2002 }
2003 goto switch_13_break;
2004 switch_13_exp_10: ;
2005 switch_13_exp_11: ;
2006 switch_13_default: ;
2007#line 1427
2008 if (s == NP) {
2009#line 1428
2010 s = SKIP1;
2011 } else {
2012 {
2013#line 1431
2014 errorFn();
2015 }
2016 }
2017 {
2018#line 1435
2019 Irp__CurrentLocation ++;
2020#line 1436
2021 Irp__Tail__Overlay__CurrentStackLocation ++;
2022#line 1437
2023 ntStatus = IofCallDriver(disketteExtension__TargetObject,
2024 Irp);
2025 }
2026#line 1440
2027 return (ntStatus);
2028 } else {
2029 switch_13_break: ;
2030 }
2031 }
2032 }
2033 }
2034 }
2035 }
2036 }
2037 }
2038 }
2039 }
2040 }
2041 }
2042 }
2043 }
2044 }
2045 }
2046 }
2047 }
2048 }
2049 }
2050 }
2051 }
2052 }
2053 }
2054 }
2055 {
2056#line 1457
2057 __cil_tmp91 = (long )ntStatus;
2058#line 1457
2059 if (__cil_tmp91 != 259L) {
2060 {
2061#line 1459
2062 Irp__IoStatus__Status___0 = ntStatus;
2063#line 1460
2064 myStatus = ntStatus;
2065#line 1461
2066 IofCompleteRequest(Irp, 0);
2067 }
2068 }
2069 }
2070#line 1466
2071 return (ntStatus);
2072}
2073}
2074#line 1469 "floppy_simpl4.cil.c"
2075int FlCheckFormatParameters(int DisketteExtension , int FormatParameters )
2076{ int DriveMediaConstants__driveMediaType__MediaType = __VERIFIER_nondet_int() ;
2077 int FormatParameters__MediaType = __VERIFIER_nondet_int() ;
2078 int FAKE_CONDITION = __VERIFIER_nondet_int() ;
2079
2080 {
2081#line 1475
2082 if (DriveMediaConstants__driveMediaType__MediaType != FormatParameters__MediaType) {
2083#line 1476
2084 return (0);
2085 } else {
2086#line 1478
2087 if (FAKE_CONDITION) {
2088#line 1479
2089 return (0);
2090 } else {
2091#line 1481
2092 return (1);
2093 }
2094 }
2095}
2096}
2097#line 1486 "floppy_simpl4.cil.c"
2098int FloppyQueueRequest(int DisketteExtension , int Irp )
2099{ int Irp__IoStatus__Status ;
2100 int Irp__IoStatus__Information ;
2101 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
2102 int ntStatus ;
2103 int FAKE_CONDITION = __VERIFIER_nondet_int() ;
2104
2105 {
2106#line 1494
2107 PagingReferenceCount ++;
2108#line 1495
2109 if (PagingReferenceCount == 1) {
2110
2111 }
2112#line 1500
2113 if (FAKE_CONDITION) {
2114 {
2115#line 1502
2116 Irp__IoStatus__Status = -1073741536;
2117#line 1503
2118 myStatus = -1073741536;
2119#line 1504
2120 Irp__IoStatus__Information = 0;
2121#line 1505
2122 IofCompleteRequest(Irp, 0);
2123#line 1506
2124 PagingReferenceCount --;
2125 }
2126#line 1508
2127 if (PagingReferenceCount == 0) {
2128
2129 }
2130#line 1513
2131 ntStatus = -1073741536;
2132 } else {
2133#line 1515
2134 Irp__IoStatus__Status = 259;
2135#line 1516
2136 myStatus = 259;
2137#line 1517
2138
2139#line 1518
2140 if (pended == 0) {
2141#line 1519
2142 pended = 1;
2143 } else {
2144 {
2145#line 1522
2146 errorFn();
2147 }
2148 }
2149#line 1525
2150 ntStatus = 259;
2151 }
2152#line 1527
2153 return (ntStatus);
2154}
2155}
2156
2157void errorFn(void)
2158{
2159
2160 {
2161 goto ERROR;
2162 ERROR:
2163#line 53
2164 return;
2165}
2166}