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