1int __VERIFIER_nondet_int() ;
2int s ;
3int UNLOADED ;
4int NP ;
5int DC ;
6int SKIP1 ;
7int SKIP2 ;
8int MPR1 ;
9int MPR3 ;
10int IPC ;
11int pended ;
12int compFptr ;
13int compRegistered ;
14int lowerDriverReturn ;
15int setEventCalled ;
16int customIrp ;
17int routine ;
18int myStatus ;
19int pirp ;
20int Executive ;
21int Suspended ;
22int KernelMode ;
23int DeviceUsageTypePaging ;
24
25void errorFn(void)
26{
27
28 {
29 goto ERROR;
30 ERROR:
31#line 60
32 return;
33}
34}
35#line 63 "cdaudio_simpl1.cil.c"
36void _BLAST_init(void)
37{
38
39 {
40#line 67
41 UNLOADED = 0;
42#line 68
43 NP = 1;
44#line 69
45 DC = 2;
46#line 70
47 SKIP1 = 3;
48#line 71
49 SKIP2 = 4;
50#line 72
51 MPR1 = 5;
52#line 73
53 MPR3 = 6;
54#line 74
55 IPC = 7;
56#line 75
57 s = UNLOADED;
58#line 76
59 pended = 0;
60#line 77
61 compFptr = 0;
62#line 78
63 compRegistered = 0;
64#line 79
65 lowerDriverReturn = 0;
66#line 80
67 setEventCalled = 0;
68#line 81
69 customIrp = 0;
70#line 82
71 return;
72}
73}
74#line 85 "cdaudio_simpl1.cil.c"
75int SendSrbSynchronous(int Extension , int Srb , int Buffer , int BufferLength )
76{ int ioStatus__Status ;
77 int ioctl ;
78 int event ;
79 int irp ;
80 int status ;
81 int __cil_tmp10 ;
82 int __cil_tmp11 ;
83 int __cil_tmp12 ;
84 int __cil_tmp13 ;
85 int __cil_tmp14 ;
86 int __cil_tmp15 ;
87 int __cil_tmp16 ;
88 int __cil_tmp17 ;
89 long __cil_tmp18 ;
90
91 {
92#line 93
93 irp = 0;
94#line 94
95 if (Buffer) {
96#line 95
97 __cil_tmp10 = 4116;
98#line 95
99 __cil_tmp11 = 49152;
100#line 95
101 __cil_tmp12 = 262144;
102#line 95
103 __cil_tmp13 = 311296;
104#line 95
105 ioctl = 315412;
106 } else {
107#line 97
108 __cil_tmp14 = 4100;
109#line 97
110 __cil_tmp15 = 49152;
111#line 97
112 __cil_tmp16 = 262144;
113#line 97
114 __cil_tmp17 = 311296;
115#line 97
116 ioctl = 315396;
117 }
118#line 99
119 if (! irp) {
120#line 100
121 return (-1073741670);
122 }
123 {
124#line 104
125 __cil_tmp18 = (long )status;
126#line 104
127 if (__cil_tmp18 == 259L) {
128 {
129#line 106
130 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
131#line 107
132 status = ioStatus__Status;
133 }
134 }
135 }
136#line 112
137 return (status);
138}
139}
140#line 115 "cdaudio_simpl1.cil.c"
141int CdAudioSignalCompletion(int DeviceObject , int Irp , int Event )
142{
143
144 {
145 {
146#line 120
147 KeSetEvent(Event, 0, 0);
148 }
149#line 122
150 return (-1073741802);
151}
152}
153#line 125 "cdaudio_simpl1.cil.c"
154int CdAudioStartDevice(int DeviceObject , int Irp )
155{ int deviceExtension__Active ;
156 int deviceExtension ;
157 int status ;
158 int srb ;
159 int srb__Cdb ;
160 int cdb ;
161 int inquiryDataPtr ;
162 int attempt ;
163 int tmp ;
164 int deviceParameterHandle ;
165 int keyValue ;
166 {
167 {
168#line 140
169 status = CdAudioForwardIrpSynchronous(DeviceObject, Irp);
170 }
171 {
172#line 142
173#line 142
174 if (status < 0) {
175#line 143
176 return (status);
177 }
178 }
179#line 147
180 if (deviceExtension__Active == 255) {
181#line 148
182 cdb = srb__Cdb;
183#line 149
184 inquiryDataPtr = 0;
185#line 150
186 attempt = 0;
187#line 151
188 if (! inquiryDataPtr) {
189#line 152
190 deviceExtension__Active = 0;
191#line 153
192 return (0);
193 }
194#line 157
195 status = -1073741823;
196 {
197#line 159
198 while (1) {
199 while_0_continue: ;
200
201 {
202#line 161
203#line 161
204 if (status < 0) {
205#line 162
206 tmp = attempt;
207#line 163
208 attempt ++;
209#line 164
210 if (tmp >= 4) {
211 goto while_0_break_1;
212 }
213 } else {
214 goto while_0_break_1;
215 }
216 }
217 {
218#line 173
219 status = SendSrbSynchronous(deviceExtension, srb, inquiryDataPtr, 36);
220 }
221 }
222 while_0_break: ;
223 }
224 while_0_break_1: ;
225 {
226#line 178
227#line 178
228 if (status < 0) {
229#line 179
230 deviceExtension__Active = 0;
231#line 180
232 return (0);
233 }
234 }
235#line 184
236 deviceExtension__Active = 0;
237 }
238#line 188
239 keyValue = deviceExtension__Active;
240 {
241#line 189
242#line 189
243 if (status < 0) {
244#line 190
245 return (0);
246 }
247 }
248 {
249#line 194
250#line 194
251 if (status < 0) {
252
253 }
254 }
255 {
256#line 200
257 ZwClose(deviceParameterHandle);
258 }
259#line 202
260 return (0);
261}
262}
263#line 205 "cdaudio_simpl1.cil.c"
264int CdAudioPnp(int DeviceObject , int Irp )
265{ int Irp__Tail__Overlay__CurrentStackLocation ;
266 int irpSp__MinorFunction ;
267 int Irp__IoStatus__Status ;
268 int irpSp__Parameters__UsageNotification__Type ;
269 int deviceExtension__PagingPathCountEvent ;
270 int irpSp__Parameters__UsageNotification__InPath ;
271 int deviceExtension__PagingPathCount ;
272 int DeviceObject__Flags ;
273 int irpSp ;
274 int status ;
275 int setPagable ;
276 int tmp ;
277 int tmp___0 ;
278
279 {
280#line 221
281 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
282#line 222
283 status = -1073741637;
284#line 223
285 if (irpSp__MinorFunction == 0) {
286 goto switch_1_0;
287 } else {
288#line 226
289 if (irpSp__MinorFunction == 22) {
290 goto switch_1_22;
291 } else {
292 goto switch_1_default;
293#line 231
294 if (0) {
295 switch_1_0:
296 {
297#line 234
298 status = CdAudioStartDevice(DeviceObject, Irp);
299#line 235
300 Irp__IoStatus__Status = status;
301#line 236
302 myStatus = status;
303#line 237
304 IofCompleteRequest(Irp, 0);
305 }
306#line 239
307 return (status);
308 switch_1_22: ;
309#line 241
310 if (irpSp__Parameters__UsageNotification__Type != DeviceUsageTypePaging) {
311 {
312#line 243
313 tmp = CdAudioSendToNextDriver(DeviceObject, Irp);
314 }
315#line 245
316 return (tmp);
317 }
318 {
319#line 250
320 status = KeWaitForSingleObject(deviceExtension__PagingPathCountEvent, Executive,
321 KernelMode, 0, 0);
322#line 252
323 setPagable = 0;
324 }
325#line 254
326 if (irpSp__Parameters__UsageNotification__InPath) {
327#line 255
328 if (deviceExtension__PagingPathCount != 1) {
329 goto _L;
330 }
331 } else {
332 _L:
333#line 262
334 if (status == status) {
335#line 265
336
337#line 266
338 setPagable = 1;
339 }
340 }
341 {
342#line 270
343 status = CdAudioForwardIrpSynchronous(DeviceObject, Irp);
344 }
345#line 272
346 if (status >= 0) {
347#line 273
348 if (irpSp__Parameters__UsageNotification__InPath) {
349
350 }
351#line 278
352 if (irpSp__Parameters__UsageNotification__InPath) {
353#line 279
354 if (deviceExtension__PagingPathCount == 1) {
355#line 280
356
357 }
358 }
359 } else {
360#line 288
361 if (setPagable == 1) {
362#line 289
363
364#line 290
365 setPagable = 0;
366 }
367 }
368 {
369#line 296
370 KeSetEvent(deviceExtension__PagingPathCountEvent, 0, 0);
371#line 297
372 IofCompleteRequest(Irp, 0);
373 }
374#line 299
375 return (status);
376 goto switch_1_break;
377 switch_1_default:
378 {
379#line 303
380 tmp___0 = CdAudioSendToNextDriver(DeviceObject, Irp);
381 }
382#line 305
383 return (tmp___0);
384 } else {
385 switch_1_break: ;
386 }
387 }
388 }
389#line 312
390 return (0);
391}
392}
393#line 315 "cdaudio_simpl1.cil.c"
394int CdAudioDeviceControl(int DeviceObject , int Irp )
395{ int deviceExtension__Active ;
396 int status ;
397
398 {
399#line 320
400 if (deviceExtension__Active == 2) {
401 goto switch_2_2;
402 } else {
403#line 323
404 if (deviceExtension__Active == 3) {
405 goto switch_2_3;
406 } else {
407#line 326
408 if (deviceExtension__Active == 1) {
409 goto switch_2_1;
410 } else {
411#line 329
412 if (deviceExtension__Active == 7) {
413 goto switch_2_7;
414 } else {
415 goto switch_2_default;
416#line 334
417 if (0) {
418 switch_2_2:
419 {
420#line 337
421 status = CdAudio535DeviceControl(DeviceObject, Irp);
422 }
423 goto switch_2_break;
424 switch_2_3:
425 {
426#line 342
427 status = CdAudio435DeviceControl(DeviceObject, Irp);
428 }
429 goto switch_2_break;
430 switch_2_1:
431 {
432#line 347
433 status = CdAudioAtapiDeviceControl(DeviceObject, Irp);
434 }
435 goto switch_2_break;
436 switch_2_7:
437 {
438#line 352
439 status = CdAudioHPCdrDeviceControl(DeviceObject, Irp);
440 }
441 goto switch_2_break;
442 switch_2_default:
443 {
444#line 357
445 deviceExtension__Active = 0;
446#line 358
447 status = CdAudioSendToNextDriver(DeviceObject, Irp);
448 }
449 } else {
450 switch_2_break: ;
451 }
452 }
453 }
454 }
455 }
456#line 368
457 return (status);
458}
459}
460#line 371 "cdaudio_simpl1.cil.c"
461int CdAudioSendToNextDriver(int DeviceObject , int Irp )
462{ int Irp__CurrentLocation ;
463 int Irp__Tail__Overlay__CurrentStackLocation ;
464 int deviceExtension__TargetDeviceObject ;
465 int tmp ;
466
467 {
468#line 378
469 if (s == NP) {
470#line 379
471 s = SKIP1;
472 } else {
473 {
474#line 382
475 errorFn();
476 }
477 }
478 {
479#line 386
480 Irp__CurrentLocation ++;
481#line 387
482 Irp__Tail__Overlay__CurrentStackLocation ++;
483#line 388
484 tmp = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
485 }
486#line 390
487 return (tmp);
488}
489}
490#line 393 "cdaudio_simpl1.cil.c"
491int CdAudioIsPlayActive(int DeviceObject )
492{ int deviceExtension__PlayActive ;
493 int ioStatus__Status ;
494 int currentBuffer__Header__AudioStatus ;
495 int irp_CdAudioIsPlayActive ;
496 int event ;
497 int status ;
498 int currentBuffer ;
499 int returnValue ;
500 long __cil_tmp10 ;
501 int __cil_tmp11 ;
502
503 {
504#line 404
505 if (! deviceExtension__PlayActive) {
506#line 405
507 return (0);
508 }
509#line 409
510 if (currentBuffer == 0) {
511#line 410
512 return (0);
513 }
514#line 414
515 if (irp_CdAudioIsPlayActive == 0) {
516#line 415
517 return (0);
518 }
519 {
520#line 419
521 __cil_tmp10 = (long )status;
522#line 419
523 if (__cil_tmp10 == 259L) {
524 {
525#line 421
526 KeWaitForSingleObject(event, Suspended, KernelMode, 0, 0);
527#line 422
528 status = ioStatus__Status;
529 }
530 }
531 }
532 {
533#line 427
534#line 427
535 if (status < 0) {
536#line 428
537 return (0);
538 }
539 }
540#line 432
541 if (currentBuffer__Header__AudioStatus == 17) {
542#line 433
543 returnValue = 1;
544 } else {
545#line 435
546 returnValue = 0;
547#line 436
548 deviceExtension__PlayActive = 0;
549 }
550#line 438
551 return (returnValue);
552}
553}
554#line 441 "cdaudio_simpl1.cil.c"
555int CdAudio535DeviceControl(int DeviceObject , int Irp )
556{ int Irp__Tail__Overlay__CurrentStackLocation ;
557 int DeviceObject__DeviceExtension ;
558 int deviceExtension__TargetDeviceObject ;
559 int Irp__AssociatedIrp__SystemBuffer ;
560 int srb__Cdb ;
561 int currentIrpStack__Parameters__DeviceIoControl__IoControlCode ;
562 int Irp__IoStatus__Information ;
563 int currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength ;
564 int currentIrpStack__Parameters__DeviceIoControl__InputBufferLength ;
565 int srb__CdbLength ;
566 int cdb__CDB10__OperationCode ;
567 int srb__TimeOutValue ;
568 int sizeof__READ_CAPACITY_DATA ;
569 int lastSession__LogicalBlockAddress ;
570 int cdaudioDataOut__FirstTrack ;
571 int cdaudioDataOut__LastTrack ;
572 int sizeof__CDROM_TOC ;
573 int sizeof__SUB_Q_CURRENT_POSITION ;
574 int userPtr__Format ;
575 int sizeof__CDROM_PLAY_AUDIO_MSF ;
576 int inputBuffer__StartingM ;
577 int inputBuffer__EndingM ;
578 int inputBuffer__StartingS ;
579 int inputBuffer__EndingS ;
580 int inputBuffer__StartingF ;
581 int inputBuffer__EndingF ;
582 int cdb__PLAY_AUDIO_MSF__OperationCode ;
583 int sizeof__CDROM_SEEK_AUDIO_MSF ;
584 int currentIrpStack ;
585 int deviceExtension ;
586 int cdaudioDataOut ;
587 int srb ;
588 int lastSession ;
589 int cdb ;
590 int status ;
591 int i ;
592 int bytesTransfered ;
593 int Toc ;
594 int tmp ;
595 int tmp___0 ;
596 int tmp___1 ;
597 int tmp___2 ;
598 int tmp___3 ;
599 int tmp___4 ;
600 int tracksToReturn ;
601 int tracksOnCd ;
602 int tracksInBuffer ;
603 int userPtr ;
604 int SubQPtr ;
605 int tmp___5 ;
606 int tmp___6 ;
607 int inputBuffer ;
608 int inputBuffer___0 ;
609 int tmp___7 ;
610 int tmp___8 ;
611 int __cil_tmp58 ;
612 int __cil_tmp59 ;
613 int __cil_tmp60 ;
614 int __cil_tmp61 ;
615 int __cil_tmp62 ;
616 int __cil_tmp63 ;
617 int __cil_tmp64 ;
618 int __cil_tmp65 ;
619 int __cil_tmp66 ;
620 int __cil_tmp67 ;
621 int __cil_tmp68 ;
622 int __cil_tmp69 ;
623 int __cil_tmp70 ;
624 int __cil_tmp71 ;
625 int __cil_tmp72 ;
626 int __cil_tmp73 ;
627 int __cil_tmp74 ;
628 int __cil_tmp75 ;
629 int __cil_tmp76 ;
630 int __cil_tmp77 ;
631 int __cil_tmp78 ;
632 int __cil_tmp79 ;
633 int __cil_tmp80 ;
634 int __cil_tmp81 ;
635 int __cil_tmp82 ;
636 int __cil_tmp83 ;
637 int __cil_tmp84 ;
638 int __cil_tmp85 ;
639 int __cil_tmp86 ;
640 int __cil_tmp87 ;
641 int __cil_tmp88 ;
642 int __cil_tmp89 ;
643 int __cil_tmp90 ;
644 int __cil_tmp91 ;
645 int __cil_tmp92 ;
646 int __cil_tmp93 ;
647 int __cil_tmp94 ;
648 int __cil_tmp95 ;
649 int __cil_tmp96 ;
650 int __cil_tmp97 ;
651 int __cil_tmp98 ;
652 int __cil_tmp99 ;
653 int __cil_tmp100 ;
654 int __cil_tmp101 ;
655 int __cil_tmp102 ;
656 int __cil_tmp103 ;
657 int __cil_tmp104 ;
658 int __cil_tmp105 ;
659 int __cil_tmp106 ;
660 unsigned long __cil_tmp107 ;
661 unsigned long __cil_tmp108 ;
662 int __cil_tmp109 ;
663 int __cil_tmp110 ;
664
665 {
666#line 499
667 currentIrpStack = Irp__Tail__Overlay__CurrentStackLocation;
668#line 500
669 deviceExtension = DeviceObject__DeviceExtension;
670#line 501
671 cdaudioDataOut = Irp__AssociatedIrp__SystemBuffer;
672#line 502
673 cdb = srb__Cdb;
674 {
675#line 503
676 __cil_tmp58 = 56;
677#line 503
678 __cil_tmp59 = 16384;
679#line 503
680 __cil_tmp60 = 131072;
681#line 503
682 __cil_tmp61 = 147456;
683#line 503
684 __cil_tmp62 = 147512;
685#line 503
686 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp62) {
687 goto switch_3_exp_0;
688 } else {
689 {
690#line 506
691 __cil_tmp63 = 16384;
692#line 506
693 __cil_tmp64 = 131072;
694#line 506
695 __cil_tmp65 = 147456;
696#line 506
697 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp65) {
698 goto switch_3_exp_1;
699 } else {
700 {
701#line 509
702 __cil_tmp66 = 44;
703#line 509
704 __cil_tmp67 = 16384;
705#line 509
706 __cil_tmp68 = 131072;
707#line 509
708 __cil_tmp69 = 147456;
709#line 509
710 __cil_tmp70 = 147500;
711#line 509
712 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp70) {
713 goto switch_3_exp_2;
714 } else {
715 {
716#line 512
717 __cil_tmp71 = 24;
718#line 512
719 __cil_tmp72 = 16384;
720#line 512
721 __cil_tmp73 = 131072;
722#line 512
723 __cil_tmp74 = 147456;
724#line 512
725 __cil_tmp75 = 147480;
726#line 512
727 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp75) {
728 goto switch_3_exp_3;
729 } else {
730 {
731#line 515
732 __cil_tmp76 = 4;
733#line 515
734 __cil_tmp77 = 16384;
735#line 515
736 __cil_tmp78 = 131072;
737#line 515
738 __cil_tmp79 = 147456;
739#line 515
740 __cil_tmp80 = 147460;
741#line 515
742 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp80) {
743 goto switch_3_exp_4;
744 } else {
745 {
746#line 518
747 __cil_tmp81 = 2056;
748#line 518
749 __cil_tmp82 = 16384;
750#line 518
751 __cil_tmp83 = 131072;
752#line 518
753 __cil_tmp84 = 147456;
754#line 518
755 __cil_tmp85 = 149512;
756#line 518
757 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp85) {
758 goto switch_3_exp_5;
759 } else {
760 {
761#line 521
762 __cil_tmp86 = 52;
763#line 521
764 __cil_tmp87 = 16384;
765#line 521
766 __cil_tmp88 = 131072;
767#line 521
768 __cil_tmp89 = 147456;
769#line 521
770 __cil_tmp90 = 147508;
771#line 521
772 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp90) {
773 goto switch_3_exp_6;
774 } else {
775 {
776#line 524
777 __cil_tmp91 = 20;
778#line 524
779 __cil_tmp92 = 16384;
780#line 524
781 __cil_tmp93 = 131072;
782#line 524
783 __cil_tmp94 = 147456;
784#line 524
785 __cil_tmp95 = 147476;
786#line 524
787 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp95) {
788 goto switch_3_exp_7;
789 } else {
790 {
791#line 527
792 __cil_tmp96 = 40;
793#line 527
794 __cil_tmp97 = 16384;
795#line 527
796 __cil_tmp98 = 131072;
797#line 527
798 __cil_tmp99 = 147456;
799#line 527
800 __cil_tmp100 = 147496;
801#line 527
802 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp100) {
803 goto switch_3_exp_8;
804 } else {
805 {
806#line 530
807 __cil_tmp101 = 2048;
808#line 530
809 __cil_tmp102 = 16384;
810#line 530
811 __cil_tmp103 = 131072;
812#line 530
813 __cil_tmp104 = 147456;
814#line 530
815 __cil_tmp105 = 149504;
816#line 530
817 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp105) {
818 goto switch_3_exp_9;
819 } else {
820 goto switch_3_default;
821#line 535
822 if (0) {
823 switch_3_exp_0:
824 {
825#line 538
826 tmp = CdAudioIsPlayActive(DeviceObject);
827 }
828#line 540
829 if (tmp) {
830#line 541
831 status = -2147483631;
832#line 542
833 Irp__IoStatus__Information = 0;
834 goto switch_3_break;
835 }
836#line 547
837 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength) {
838#line 548
839 status = -1073741789;
840#line 549
841 Irp__IoStatus__Information = 0;
842 goto switch_3_break;
843 }
844#line 554
845 if (lastSession == 0) {
846 {
847#line 556
848 status = -1073741670;
849#line 557
850 Irp__IoStatus__Information = 0;
851#line 558
852 tmp___0 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
853 }
854#line 560
855 return (tmp___0);
856 }
857 {
858#line 565
859 srb__CdbLength = 10;
860#line 566
861 cdb__CDB10__OperationCode = 38;
862#line 567
863 srb__TimeOutValue = 10;
864#line 568
865 status = SendSrbSynchronous(deviceExtension, srb, lastSession,
866 sizeof__READ_CAPACITY_DATA);
867 }
868 {
869#line 571
870#line 571
871 if (status < 0) {
872 {
873#line 573
874 Irp__IoStatus__Information = 0;
875#line 574
876 tmp___1 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
877 }
878#line 576
879 return (tmp___1);
880 } else {
881#line 578
882 status = 0;
883 }
884 }
885#line 580
886 Irp__IoStatus__Information = bytesTransfered;
887#line 581
888 if (lastSession__LogicalBlockAddress == 0) {
889 goto switch_3_break;
890 }
891#line 586
892 cdaudioDataOut__FirstTrack = 1;
893#line 587
894 cdaudioDataOut__LastTrack = 2;
895 goto switch_3_break;
896 switch_3_exp_1: ;
897#line 590
898 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength) {
899#line 591
900 status = -1073741789;
901#line 592
902 Irp__IoStatus__Information = 0;
903 goto switch_3_break;
904 }
905 {
906#line 598
907 tmp___2 = CdAudioIsPlayActive(DeviceObject);
908 }
909#line 600
910 if (tmp___2) {
911#line 601
912 status = -2147483631;
913#line 602
914 Irp__IoStatus__Information = 0;
915 goto switch_3_break;
916 }
917#line 607
918 if (Toc == 0) {
919 {
920#line 609
921 status = -1073741670;
922#line 610
923 Irp__IoStatus__Information = 0;
924#line 611
925 tmp___3 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
926 }
927#line 613
928 return (tmp___3);
929 }
930 {
931#line 618
932 srb__TimeOutValue = 10;
933#line 619
934 srb__CdbLength = 10;
935#line 620
936 status = SendSrbSynchronous(deviceExtension, srb, Toc, sizeof__CDROM_TOC);
937 }
938#line 622
939 if (status >= 0) {
940 {
941#line 623
942 __cil_tmp107 = (unsigned long )status;
943#line 623
944 if (__cil_tmp107 != -1073741764) {
945#line 624
946 status = 0;
947 } else {
948 goto _L;
949 }
950 }
951 } else {
952 _L:
953 {
954#line 630
955 __cil_tmp108 = (unsigned long )status;
956#line 630
957 if (__cil_tmp108 != -1073741764) {
958 {
959#line 632
960 Irp__IoStatus__Information = 0;
961#line 633
962 tmp___4 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
963 }
964#line 635
965 return (tmp___4);
966 }
967 }
968 }
969#line 640
970 __cil_tmp109 = cdaudioDataOut__LastTrack - cdaudioDataOut__FirstTrack;
971#line 640
972 tracksOnCd = __cil_tmp109 + 1;
973#line 641
974 tracksInBuffer = currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength;
975#line 642
976 if (tracksInBuffer < tracksOnCd) {
977#line 643
978 tracksToReturn = tracksInBuffer;
979 } else {
980#line 645
981 tracksToReturn = tracksOnCd;
982 }
983#line 647
984 if (tracksInBuffer > tracksOnCd) {
985#line 648
986 i ++;
987 }
988 goto switch_3_break;
989 switch_3_exp_2:
990#line 654
991 userPtr = Irp__AssociatedIrp__SystemBuffer;
992#line 655
993 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength < sizeof__SUB_Q_CURRENT_POSITION) {
994#line 656
995 status = -1073741789;
996#line 657
997 Irp__IoStatus__Information = 0;
998 goto switch_3_break;
999 }
1000#line 662
1001 if (SubQPtr == 0) {
1002 {
1003#line 664
1004 status = -1073741670;
1005#line 665
1006 Irp__IoStatus__Information = 0;
1007#line 666
1008 tmp___5 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
1009 }
1010#line 668
1011 return (tmp___5);
1012 }
1013#line 672
1014 if (userPtr__Format != 1) {
1015 {
1016#line 674
1017 status = -1073741823;
1018#line 675
1019 Irp__IoStatus__Information = 0;
1020#line 676
1021 tmp___6 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
1022 }
1023#line 678
1024 return (tmp___6);
1025 }
1026 {
1027#line 683
1028 srb__CdbLength = 10;
1029#line 684
1030 srb__TimeOutValue = 10;
1031#line 685
1032 status = SendSrbSynchronous(deviceExtension, srb, SubQPtr,
1033 sizeof__SUB_Q_CURRENT_POSITION);
1034 }
1035#line 688
1036 if (status >= 0) {
1037#line 689
1038 Irp__IoStatus__Information = sizeof__SUB_Q_CURRENT_POSITION;
1039 } else {
1040#line 691
1041 Irp__IoStatus__Information = 0;
1042 }
1043 goto switch_3_break;
1044 switch_3_exp_3:
1045#line 695
1046 inputBuffer = Irp__AssociatedIrp__SystemBuffer;
1047#line 696
1048 Irp__IoStatus__Information = 0;
1049#line 697
1050 if (currentIrpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CDROM_PLAY_AUDIO_MSF) {
1051#line 698
1052 status = -1073741820;
1053 goto switch_3_break;
1054 }
1055#line 703
1056 if (inputBuffer__StartingM == inputBuffer__EndingM) {
1057#line 704
1058 if (inputBuffer__StartingS == inputBuffer__EndingS) {
1059#line 705
1060 if (inputBuffer__StartingF == inputBuffer__EndingF) {
1061
1062 }
1063 }
1064 }
1065 {
1066#line 717
1067 srb__CdbLength = 10;
1068#line 718
1069 srb__TimeOutValue = 10;
1070#line 719
1071 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1072 }
1073#line 721
1074 if (status >= 0) {
1075#line 722
1076 if (cdb__PLAY_AUDIO_MSF__OperationCode == 71) {
1077
1078 }
1079 }
1080 goto switch_3_break;
1081 switch_3_exp_4:
1082#line 732
1083 inputBuffer___0 = Irp__AssociatedIrp__SystemBuffer;
1084#line 733
1085 Irp__IoStatus__Information = 0;
1086#line 734
1087 if (currentIrpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CDROM_SEEK_AUDIO_MSF) {
1088#line 735
1089 status = -1073741820;
1090 goto switch_3_break;
1091 }
1092 {
1093#line 741
1094 srb__CdbLength = 10;
1095#line 742
1096 srb__TimeOutValue = 10;
1097#line 743
1098 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1099 }
1100 {
1101#line 745
1102#line 745
1103 if (status < 0) {
1104
1105 }
1106 }
1107 goto switch_3_break;
1108 switch_3_exp_5:
1109 {
1110#line 753
1111 Irp__IoStatus__Information = 0;
1112#line 754
1113 srb__CdbLength = 10;
1114#line 755
1115 srb__TimeOutValue = 10;
1116#line 756
1117 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1118 }
1119 goto switch_3_break;
1120 switch_3_exp_6: ;
1121 switch_3_exp_7: ;
1122 switch_3_exp_8:
1123#line 762
1124 Irp__IoStatus__Information = 0;
1125#line 763
1126 status = -1073741808;
1127 goto switch_3_break;
1128 switch_3_exp_9:
1129 {
1130#line 767
1131 CdAudioIsPlayActive(DeviceObject);
1132 }
1133 switch_3_default:
1134 {
1135#line 771
1136 tmp___7 = CdAudioSendToNextDriver(DeviceObject, Irp);
1137 }
1138#line 773
1139 return (tmp___7);
1140 goto switch_3_break;
1141 } else {
1142 switch_3_break: ;
1143 }
1144 }
1145 }
1146 }
1147 }
1148 }
1149 }
1150 }
1151 }
1152 }
1153 }
1154 }
1155 }
1156 }
1157 }
1158 }
1159 }
1160 }
1161 }
1162 }
1163 }
1164 {
1165#line 790
1166 tmp___8 = AG_SetStatusAndReturn(status, Irp, deviceExtension__TargetDeviceObject);
1167 }
1168#line 792
1169 return (tmp___8);
1170}
1171}
1172#line 795 "cdaudio_simpl1.cil.c"
1173int AG_SetStatusAndReturn(int status , int Irp , int deviceExtension__TargetDeviceObject )
1174{ unsigned long __cil_tmp4 ;
1175
1176 {
1177 {
1178#line 799
1179 __cil_tmp4 = (unsigned long )status;
1180#line 799
1181 if (__cil_tmp4 == -2147483626) {
1182
1183 }
1184 }
1185 {
1186#line 805
1187 myStatus = status;
1188#line 806
1189 IofCompleteRequest(Irp, 0);
1190 }
1191#line 808
1192 return (status);
1193}
1194}
1195#line 811 "cdaudio_simpl1.cil.c"
1196int CdAudio435DeviceControl(int DeviceObject , int Irp )
1197{ int currentIrpStack__Parameters__DeviceIoControl__IoControlCode ;
1198 int currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength ;
1199 int currentIrpStack__Parameters__DeviceIoControl__InputBufferLength ;
1200 int TrackData__0 ;
1201 int Irp__IoStatus__Information ;
1202 int srb__TimeOutValue ;
1203 int srb__CdbLength ;
1204 int sizeof__CDROM_TOC ;
1205 int cdaudioDataOut__LastTrack ;
1206 int cdaudioDataOut__FirstTrack ;
1207 int sizeof__CDROM_PLAY_AUDIO_MSF ;
1208 int sizeof__CDROM_SEEK_AUDIO_MSF ;
1209 int deviceExtension__Paused ;
1210 int deviceExtension__PlayActive ;
1211 int sizeof__SUB_Q_CHANNEL_DATA ;
1212 int sizeof__SUB_Q_CURRENT_POSITION ;
1213 int deviceExtension ;
1214 int srb ;
1215 int status ;
1216 int i ;
1217 int bytesTransfered ;
1218 int Toc ;
1219 int tmp ;
1220 int tracksToReturn ;
1221 int tracksOnCd ;
1222 int tracksInBuffer ;
1223 int SubQPtr ;
1224 int userPtr__Format ;
1225 int SubQPtr___0 ;
1226 int tmp___0 ;
1227 int tmp___1 ;
1228 int tmp___2 ;
1229 int __cil_tmp35 ;
1230 int __cil_tmp36 ;
1231 int __cil_tmp37 ;
1232 int __cil_tmp38 ;
1233 int __cil_tmp39 ;
1234 int __cil_tmp40 ;
1235 int __cil_tmp41 ;
1236 int __cil_tmp42 ;
1237 int __cil_tmp43 ;
1238 int __cil_tmp44 ;
1239 int __cil_tmp45 ;
1240 int __cil_tmp46 ;
1241 int __cil_tmp47 ;
1242 int __cil_tmp48 ;
1243 int __cil_tmp49 ;
1244 int __cil_tmp50 ;
1245 int __cil_tmp51 ;
1246 int __cil_tmp52 ;
1247 int __cil_tmp53 ;
1248 int __cil_tmp54 ;
1249 int __cil_tmp55 ;
1250 int __cil_tmp56 ;
1251 int __cil_tmp57 ;
1252 int __cil_tmp58 ;
1253 int __cil_tmp59 ;
1254 int __cil_tmp60 ;
1255 int __cil_tmp61 ;
1256 int __cil_tmp62 ;
1257 int __cil_tmp63 ;
1258 int __cil_tmp64 ;
1259 int __cil_tmp65 ;
1260 int __cil_tmp66 ;
1261 int __cil_tmp67 ;
1262 int __cil_tmp68 ;
1263 int __cil_tmp69 ;
1264 int __cil_tmp70 ;
1265 int __cil_tmp71 ;
1266 int __cil_tmp72 ;
1267 int __cil_tmp73 ;
1268 int __cil_tmp74 ;
1269 int __cil_tmp75 ;
1270 int __cil_tmp76 ;
1271 int __cil_tmp77 ;
1272 int __cil_tmp78 ;
1273 int __cil_tmp79 ;
1274 int __cil_tmp80 ;
1275 int __cil_tmp81 ;
1276 int __cil_tmp82 ;
1277 int __cil_tmp83 ;
1278 int __cil_tmp84 ;
1279 int __cil_tmp85 ;
1280 int __cil_tmp86 ;
1281 int __cil_tmp87 ;
1282 int __cil_tmp88 ;
1283 int __cil_tmp89 ;
1284 int __cil_tmp90 ;
1285 int __cil_tmp91 ;
1286 int __cil_tmp92 ;
1287 unsigned long __cil_tmp93 ;
1288 int __cil_tmp94 ;
1289 unsigned long __cil_tmp95 ;
1290 unsigned long __cil_tmp96 ;
1291 unsigned long __cil_tmp97 ;
1292 int __cil_tmp98 ;
1293 int __cil_tmp99 ;
1294 int __cil_tmp100 ;
1295 int __cil_tmp101 ;
1296 int __cil_tmp102 ;
1297 int __cil_tmp103 ;
1298 unsigned long __cil_tmp104 ;
1299 unsigned long __cil_tmp105 ;
1300 unsigned long __cil_tmp106 ;
1301 unsigned long __cil_tmp107 ;
1302 int __cil_tmp108 ;
1303 unsigned long __cil_tmp109 ;
1304 int __cil_tmp110 ;
1305 unsigned long __cil_tmp111 ;
1306 unsigned long __cil_tmp112 ;
1307 unsigned long __cil_tmp113 ;
1308 unsigned long __cil_tmp114 ;
1309 unsigned long __cil_tmp115 ;
1310 unsigned long __cil_tmp116 ;
1311
1312 {
1313 {
1314#line 846
1315 __cil_tmp35 = 16384;
1316#line 846
1317 __cil_tmp36 = 131072;
1318#line 846
1319 __cil_tmp37 = 147456;
1320#line 846
1321 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp37) {
1322 goto switch_4_exp_10;
1323 } else {
1324 {
1325#line 849
1326 __cil_tmp38 = 24;
1327#line 849
1328 __cil_tmp39 = 16384;
1329#line 849
1330 __cil_tmp40 = 131072;
1331#line 849
1332 __cil_tmp41 = 147456;
1333#line 849
1334 __cil_tmp42 = 147480;
1335#line 849
1336 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp42) {
1337 goto switch_4_exp_11;
1338 } else {
1339 {
1340#line 852
1341 __cil_tmp43 = 8;
1342#line 852
1343 __cil_tmp44 = 16384;
1344#line 852
1345 __cil_tmp45 = 131072;
1346#line 852
1347 __cil_tmp46 = 147456;
1348#line 852
1349 __cil_tmp47 = 147464;
1350#line 852
1351 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp47) {
1352 goto switch_4_exp_12;
1353 } else {
1354 {
1355#line 855
1356 __cil_tmp48 = 4;
1357#line 855
1358 __cil_tmp49 = 16384;
1359#line 855
1360 __cil_tmp50 = 131072;
1361#line 855
1362 __cil_tmp51 = 147456;
1363#line 855
1364 __cil_tmp52 = 147460;
1365#line 855
1366 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp52) {
1367 goto switch_4_exp_13;
1368 } else {
1369 {
1370#line 858
1371 __cil_tmp53 = 12;
1372#line 858
1373 __cil_tmp54 = 16384;
1374#line 858
1375 __cil_tmp55 = 131072;
1376#line 858
1377 __cil_tmp56 = 147456;
1378#line 858
1379 __cil_tmp57 = 147468;
1380#line 858
1381 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp57) {
1382 goto switch_4_exp_14;
1383 } else {
1384 {
1385#line 861
1386 __cil_tmp58 = 16;
1387#line 861
1388 __cil_tmp59 = 16384;
1389#line 861
1390 __cil_tmp60 = 131072;
1391#line 861
1392 __cil_tmp61 = 147456;
1393#line 861
1394 __cil_tmp62 = 147472;
1395#line 861
1396 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp62) {
1397 goto switch_4_exp_15;
1398 } else {
1399 {
1400#line 864
1401 __cil_tmp63 = 44;
1402#line 864
1403 __cil_tmp64 = 16384;
1404#line 864
1405 __cil_tmp65 = 131072;
1406#line 864
1407 __cil_tmp66 = 147456;
1408#line 864
1409 __cil_tmp67 = 147500;
1410#line 864
1411 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp67) {
1412 goto switch_4_exp_16;
1413 } else {
1414 {
1415#line 867
1416 __cil_tmp68 = 2056;
1417#line 867
1418 __cil_tmp69 = 16384;
1419#line 867
1420 __cil_tmp70 = 131072;
1421#line 867
1422 __cil_tmp71 = 147456;
1423#line 867
1424 __cil_tmp72 = 149512;
1425#line 867
1426 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp72) {
1427 goto switch_4_exp_17;
1428 } else {
1429 {
1430#line 870
1431 __cil_tmp73 = 52;
1432#line 870
1433 __cil_tmp74 = 16384;
1434#line 870
1435 __cil_tmp75 = 131072;
1436#line 870
1437 __cil_tmp76 = 147456;
1438#line 870
1439 __cil_tmp77 = 147508;
1440#line 870
1441 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp77) {
1442 goto switch_4_exp_18;
1443 } else {
1444 {
1445#line 873
1446 __cil_tmp78 = 20;
1447#line 873
1448 __cil_tmp79 = 16384;
1449#line 873
1450 __cil_tmp80 = 131072;
1451#line 873
1452 __cil_tmp81 = 147456;
1453#line 873
1454 __cil_tmp82 = 147476;
1455#line 873
1456 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp82) {
1457 goto switch_4_exp_19;
1458 } else {
1459 {
1460#line 876
1461 __cil_tmp83 = 40;
1462#line 876
1463 __cil_tmp84 = 16384;
1464#line 876
1465 __cil_tmp85 = 131072;
1466#line 876
1467 __cil_tmp86 = 147456;
1468#line 876
1469 __cil_tmp87 = 147496;
1470#line 876
1471 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp87) {
1472 goto switch_4_exp_20;
1473 } else {
1474 {
1475#line 879
1476 __cil_tmp88 = 2048;
1477#line 879
1478 __cil_tmp89 = 16384;
1479#line 879
1480 __cil_tmp90 = 131072;
1481#line 879
1482 __cil_tmp91 = 147456;
1483#line 879
1484 __cil_tmp92 = 149504;
1485#line 879
1486 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp92) {
1487 goto switch_4_exp_21;
1488 } else {
1489 goto switch_4_default;
1490#line 884
1491 if (0) {
1492 switch_4_exp_10: ;
1493#line 886
1494 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength < TrackData__0) {
1495#line 887
1496 status = -1073741789;
1497#line 888
1498 Irp__IoStatus__Information = 0;
1499 goto switch_4_break;
1500 }
1501 {
1502#line 894
1503 tmp = CdAudioIsPlayActive(DeviceObject);
1504 }
1505#line 896
1506 if (tmp) {
1507#line 897
1508 status = -2147483631;
1509#line 898
1510 Irp__IoStatus__Information = 0;
1511 goto switch_4_break;
1512 }
1513#line 903
1514 if (Toc == 0) {
1515#line 904
1516 status = -1073741670;
1517#line 905
1518 Irp__IoStatus__Information = 0;
1519 {
1520#line 906
1521 __cil_tmp93 = (unsigned long )status;
1522#line 906
1523 if (__cil_tmp93 == -2147483626) {
1524#line 907
1525 Irp__IoStatus__Information = 0;
1526 }
1527 }
1528 {
1529#line 912
1530 myStatus = status;
1531#line 913
1532 IofCompleteRequest(Irp, 0);
1533 }
1534#line 915
1535 return (status);
1536 }
1537 {
1538#line 920
1539 srb__TimeOutValue = 10;
1540#line 921
1541 srb__CdbLength = 10;
1542#line 922
1543 status = SendSrbSynchronous(deviceExtension, srb, Toc,
1544 sizeof__CDROM_TOC);
1545 }
1546 {
1547#line 925
1548#line 925
1549 if (status < 0) {
1550 {
1551#line 926
1552 __cil_tmp95 = (unsigned long )status;
1553#line 926
1554 if (__cil_tmp95 != -1073741764) {
1555 {
1556#line 927
1557 __cil_tmp96 = (unsigned long )status;
1558#line 927
1559 if (__cil_tmp96 != -1073741764) {
1560 {
1561#line 928
1562 __cil_tmp97 = (unsigned long )status;
1563#line 928
1564 if (__cil_tmp97 == -2147483626) {
1565#line 929
1566 Irp__IoStatus__Information = 0;
1567 }
1568 }
1569 {
1570#line 934
1571 myStatus = status;
1572#line 935
1573 IofCompleteRequest(Irp, 0);
1574 }
1575#line 937
1576 return (status);
1577 }
1578 }
1579 } else {
1580#line 942
1581 status = 0;
1582 }
1583 }
1584 } else {
1585#line 945
1586 status = 0;
1587 }
1588 }
1589#line 947
1590 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength > sizeof__CDROM_TOC) {
1591#line 948
1592 bytesTransfered = sizeof__CDROM_TOC;
1593 } else {
1594#line 950
1595 bytesTransfered = currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength;
1596 }
1597#line 952
1598 __cil_tmp98 = cdaudioDataOut__LastTrack - cdaudioDataOut__FirstTrack;
1599#line 952
1600 tracksOnCd = __cil_tmp98 + 1;
1601#line 953
1602 tracksInBuffer = currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength - TrackData__0;
1603#line 954
1604 if (tracksInBuffer < tracksOnCd) {
1605#line 955
1606 tracksToReturn = tracksInBuffer;
1607 } else {
1608#line 957
1609 tracksToReturn = tracksOnCd;
1610 }
1611#line 959
1612 if (tracksInBuffer > tracksOnCd) {
1613#line 960
1614 i ++;
1615 }
1616 goto switch_4_break;
1617 switch_4_exp_11: ;
1618 switch_4_exp_12:
1619 {
1620#line 968
1621 Irp__IoStatus__Information = 0;
1622#line 969
1623 srb__CdbLength = 10;
1624#line 970
1625 srb__TimeOutValue = 10;
1626#line 971
1627 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1628 }
1629#line 973
1630 if (status >= 0) {
1631
1632 }
1633 {
1634#line 978
1635 __cil_tmp99 = 8;
1636#line 978
1637 __cil_tmp100 = 16384;
1638#line 978
1639 __cil_tmp101 = 131072;
1640#line 978
1641 __cil_tmp102 = 147456;
1642#line 978
1643 __cil_tmp103 = 147464;
1644#line 978
1645 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp103) {
1646 {
1647#line 979
1648 __cil_tmp104 = (unsigned long )status;
1649#line 979
1650 if (__cil_tmp104 == -2147483626) {
1651#line 980
1652 Irp__IoStatus__Information = 0;
1653 }
1654 }
1655 {
1656#line 985
1657 myStatus = status;
1658#line 986
1659 IofCompleteRequest(Irp, 0);
1660 }
1661#line 988
1662 return (status);
1663 }
1664 }
1665#line 992
1666 if (currentIrpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CDROM_PLAY_AUDIO_MSF) {
1667#line 993
1668 status = -1073741820;
1669 goto switch_4_break;
1670 }
1671 {
1672#line 999
1673 srb__CdbLength = 10;
1674#line 1000
1675 srb__TimeOutValue = 10;
1676#line 1001
1677 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1678 }
1679#line 1003
1680 if (status >= 0) {
1681
1682 }
1683 goto switch_4_break;
1684 switch_4_exp_13:
1685#line 1010
1686 Irp__IoStatus__Information = 0;
1687#line 1011
1688 if (currentIrpStack__Parameters__DeviceIoControl__InputBufferLength < sizeof__CDROM_SEEK_AUDIO_MSF) {
1689#line 1012
1690 status = -1073741820;
1691 goto switch_4_break;
1692 }
1693 {
1694#line 1018
1695 srb__CdbLength = 10;
1696#line 1019
1697 srb__TimeOutValue = 10;
1698#line 1020
1699 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1700 }
1701#line 1022
1702 if (status < 0) {
1703 {
1704#line 1025
1705 __cil_tmp105 = (unsigned long )status;
1706#line 1025
1707 if (__cil_tmp105 == -1073741808) {
1708#line 1026
1709 status = -1073741803;
1710 }
1711 }
1712 }
1713 goto switch_4_break;
1714 switch_4_exp_14:
1715#line 1033
1716 Irp__IoStatus__Information = 0;
1717#line 1034
1718 if (SubQPtr == 0) {
1719#line 1035
1720 status = -1073741670;
1721 {
1722#line 1036
1723 __cil_tmp106 = (unsigned long )status;
1724#line 1036
1725 if (__cil_tmp106 == -2147483626) {
1726#line 1037
1727 Irp__IoStatus__Information = 0;
1728 }
1729 }
1730 {
1731#line 1042
1732 myStatus = status;
1733#line 1043
1734 IofCompleteRequest(Irp, 0);
1735 }
1736#line 1045
1737 return (status);
1738 }
1739#line 1049
1740 if (deviceExtension__Paused == 1) {
1741#line 1050
1742 status = 0;
1743 {
1744#line 1051
1745 __cil_tmp107 = (unsigned long )status;
1746#line 1051
1747 if (__cil_tmp107 == -2147483626) {
1748#line 1052
1749 Irp__IoStatus__Information = 0;
1750 }
1751 }
1752 {
1753#line 1057
1754 myStatus = status;
1755#line 1058
1756 IofCompleteRequest(Irp, 0);
1757 }
1758#line 1060
1759 return (status);
1760 }
1761 {
1762#line 1065
1763 srb__CdbLength = 10;
1764#line 1066
1765 srb__TimeOutValue = 10;
1766#line 1067
1767 status = SendSrbSynchronous(deviceExtension, srb, SubQPtr,
1768 sizeof__SUB_Q_CHANNEL_DATA);
1769 }
1770 {
1771#line 1070
1772#line 1070
1773 if (status < 0) {
1774 {
1775#line 1071
1776 __cil_tmp109 = (unsigned long )status;
1777#line 1071
1778 if (__cil_tmp109 == -2147483626) {
1779#line 1072
1780 Irp__IoStatus__Information = 0;
1781 }
1782 }
1783 {
1784#line 1077
1785 myStatus = status;
1786#line 1078
1787 IofCompleteRequest(Irp, 0);
1788 }
1789#line 1080
1790 return (status);
1791 }
1792 }
1793 {
1794#line 1085
1795 srb__CdbLength = 10;
1796#line 1086
1797 srb__TimeOutValue = 10;
1798#line 1087
1799 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1800 }
1801 {
1802#line 1089
1803#line 1089
1804 if (status < 0) {
1805 {
1806#line 1090
1807 __cil_tmp111 = (unsigned long )status;
1808#line 1090
1809 if (__cil_tmp111 == -2147483626) {
1810#line 1091
1811 Irp__IoStatus__Information = 0;
1812 }
1813 }
1814 {
1815#line 1096
1816 myStatus = status;
1817#line 1097
1818 IofCompleteRequest(Irp, 0);
1819 }
1820#line 1099
1821 return (status);
1822 }
1823 }
1824 goto switch_4_break;
1825 switch_4_exp_15:
1826#line 1105
1827 Irp__IoStatus__Information = 0;
1828#line 1106
1829 if (deviceExtension__Paused == 0) {
1830#line 1107
1831 status = -1073741823;
1832 {
1833#line 1108
1834 __cil_tmp112 = (unsigned long )status;
1835#line 1108
1836 if (__cil_tmp112 == -2147483626) {
1837#line 1109
1838 Irp__IoStatus__Information = 0;
1839 }
1840 }
1841 {
1842#line 1114
1843 myStatus = status;
1844#line 1115
1845 IofCompleteRequest(Irp, 0);
1846 }
1847#line 1117
1848 return (status);
1849 }
1850 {
1851#line 1122
1852 srb__CdbLength = 10;
1853#line 1123
1854 srb__TimeOutValue = 10;
1855#line 1124
1856 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1857 }
1858#line 1126
1859 if (status >= 0) {
1860#line 1127
1861 deviceExtension__PlayActive = 1;
1862#line 1128
1863 deviceExtension__Paused = 0;
1864 }
1865 goto switch_4_break;
1866 switch_4_exp_16: ;
1867#line 1134
1868 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength < sizeof__SUB_Q_CURRENT_POSITION) {
1869#line 1135
1870 status = -1073741789;
1871#line 1136
1872 Irp__IoStatus__Information = 0;
1873 goto switch_4_break;
1874 }
1875#line 1141
1876 if (SubQPtr___0 == 0) {
1877#line 1142
1878 status = -1073741670;
1879#line 1143
1880 Irp__IoStatus__Information = 0;
1881 {
1882#line 1144
1883 __cil_tmp113 = (unsigned long )status;
1884#line 1144
1885 if (__cil_tmp113 == -2147483626) {
1886#line 1145
1887 Irp__IoStatus__Information = 0;
1888 }
1889 }
1890 {
1891#line 1150
1892 myStatus = status;
1893#line 1151
1894 IofCompleteRequest(Irp, 0);
1895 }
1896#line 1153
1897 return (status);
1898 }
1899#line 1157
1900 if (userPtr__Format != 1) {
1901#line 1158
1902 status = -1073741823;
1903#line 1159
1904 Irp__IoStatus__Information = 0;
1905 {
1906#line 1160
1907 __cil_tmp114 = (unsigned long )status;
1908#line 1160
1909 if (__cil_tmp114 == -2147483626) {
1910#line 1161
1911 Irp__IoStatus__Information = 0;
1912 }
1913 }
1914 {
1915#line 1166
1916 myStatus = status;
1917#line 1167
1918 IofCompleteRequest(Irp, 0);
1919 }
1920#line 1169
1921 return (status);
1922 }
1923 {
1924#line 1174
1925 srb__CdbLength = 10;
1926#line 1175
1927 srb__TimeOutValue = 10;
1928#line 1176
1929 status = SendSrbSynchronous(deviceExtension, srb, SubQPtr___0,
1930 sizeof__SUB_Q_CHANNEL_DATA);
1931 }
1932#line 1179
1933 if (status >= 0) {
1934#line 1180
1935 if (deviceExtension__Paused == 1) {
1936#line 1181
1937 deviceExtension__PlayActive = 0;
1938 }
1939#line 1185
1940 Irp__IoStatus__Information = sizeof__SUB_Q_CURRENT_POSITION;
1941 } else {
1942#line 1187
1943 Irp__IoStatus__Information = 0;
1944 }
1945 goto switch_4_break;
1946 switch_4_exp_17:
1947 {
1948#line 1192
1949 Irp__IoStatus__Information = 0;
1950#line 1193
1951 srb__CdbLength = 10;
1952#line 1194
1953 srb__TimeOutValue = 10;
1954#line 1195
1955 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
1956 }
1957 goto switch_4_break;
1958 switch_4_exp_18: ;
1959 switch_4_exp_19: ;
1960 switch_4_exp_20:
1961#line 1201
1962 Irp__IoStatus__Information = 0;
1963#line 1202
1964 status = -1073741808;
1965 goto switch_4_break;
1966 switch_4_exp_21:
1967 {
1968#line 1206
1969 tmp___1 = CdAudioIsPlayActive(DeviceObject);
1970 }
1971#line 1208
1972 if (tmp___1 == 1) {
1973#line 1209
1974 deviceExtension__PlayActive = 1;
1975#line 1210
1976 status = 0;
1977#line 1211
1978 Irp__IoStatus__Information = 0;
1979 {
1980#line 1212
1981 __cil_tmp115 = (unsigned long )status;
1982#line 1212
1983 if (__cil_tmp115 == -2147483626) {
1984#line 1213
1985 Irp__IoStatus__Information = 0;
1986 }
1987 }
1988 {
1989#line 1218
1990 myStatus = status;
1991#line 1219
1992 IofCompleteRequest(Irp, 0);
1993 }
1994#line 1221
1995 return (status);
1996 } else {
1997 {
1998#line 1224
1999 deviceExtension__PlayActive = 0;
2000#line 1225
2001 tmp___0 = CdAudioSendToNextDriver(DeviceObject, Irp);
2002 }
2003#line 1227
2004 return (tmp___0);
2005 }
2006 goto switch_4_break;
2007 switch_4_default:
2008 {
2009#line 1232
2010 tmp___2 = CdAudioSendToNextDriver(DeviceObject, Irp);
2011 }
2012#line 1234
2013 return (tmp___2);
2014 goto switch_4_break;
2015 } else {
2016 switch_4_break: ;
2017 }
2018 }
2019 }
2020 }
2021 }
2022 }
2023 }
2024 }
2025 }
2026 }
2027 }
2028 }
2029 }
2030 }
2031 }
2032 }
2033 }
2034 }
2035 }
2036 }
2037 }
2038 }
2039 }
2040 }
2041 }
2042 {
2043#line 1252
2044 __cil_tmp116 = (unsigned long )status;
2045#line 1252
2046 if (__cil_tmp116 == -2147483626) {
2047#line 1253
2048 Irp__IoStatus__Information = 0;
2049 }
2050 }
2051 {
2052#line 1258
2053 myStatus = status;
2054#line 1259
2055 IofCompleteRequest(Irp, 0);
2056 }
2057#line 1261
2058 return (status);
2059}
2060}
2061#line 1264 "cdaudio_simpl1.cil.c"
2062int CdAudioAtapiDeviceControl(int DeviceObject , int Irp )
2063{ int currentIrpStack__Parameters__DeviceIoControl__IoControlCode ;
2064 int Irp__IoStatus__Information ;
2065 int deviceExtension__PlayActive ;
2066 int srb__CdbLength ;
2067 int srb__TimeOutValue ;
2068 int Irp__IoStatus__Status ;
2069 int status ;
2070 int deviceExtension ;
2071 int srb ;
2072 int tmp ;
2073 int __cil_tmp13 ;
2074 int __cil_tmp14 ;
2075 int __cil_tmp15 ;
2076 int __cil_tmp16 ;
2077 int __cil_tmp17 ;
2078 int __cil_tmp18 ;
2079
2080 {
2081 {
2082#line 1277
2083 __cil_tmp13 = 8;
2084#line 1277
2085 __cil_tmp14 = 16384;
2086#line 1277
2087 __cil_tmp15 = 131072;
2088#line 1277
2089 __cil_tmp16 = 147456;
2090#line 1277
2091 __cil_tmp17 = 147464;
2092#line 1277
2093 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp17) {
2094 {
2095#line 1279
2096 Irp__IoStatus__Information = 0;
2097#line 1280
2098 deviceExtension__PlayActive = 0;
2099#line 1281
2100 srb__CdbLength = 12;
2101#line 1282
2102 srb__TimeOutValue = 10;
2103#line 1283
2104 status = SendSrbSynchronous(deviceExtension, srb, 0, 0);
2105 }
2106 {
2107#line 1285
2108#line 1285
2109 if (status < 0) {
2110 {
2111#line 1287
2112 Irp__IoStatus__Status = status;
2113#line 1288
2114 myStatus = status;
2115#line 1289
2116 IofCompleteRequest(Irp, 0);
2117 }
2118#line 1291
2119 return (status);
2120 }
2121 }
2122 } else {
2123 {
2124#line 1297
2125 tmp = CdAudioSendToNextDriver(DeviceObject, Irp);
2126 }
2127#line 1299
2128 return (tmp);
2129 }
2130 }
2131 {
2132#line 1302
2133 Irp__IoStatus__Status = status;
2134#line 1303
2135 myStatus = status;
2136#line 1304
2137 IofCompleteRequest(Irp, 0);
2138 }
2139#line 1306
2140 return (status);
2141}
2142}
2143#line 1309 "cdaudio_simpl1.cil.c"
2144void HpCdrProcessLastSession(int Toc )
2145{ int index ;
2146
2147 {
2148#line 1313
2149 if (index) {
2150#line 1314
2151 index --;
2152 }
2153#line 1318
2154 return;
2155}
2156}
2157#line 1321 "cdaudio_simpl1.cil.c"
2158int HPCdrCompletion(int DeviceObject , int Irp , int Context )
2159{ int Irp__PendingReturned ;
2160 int Irp__AssociatedIrp__SystemBuffer ;
2161
2162 {
2163#line 1326
2164 if (Irp__PendingReturned) {
2165#line 1327
2166 if (pended == 0) {
2167#line 1328
2168 pended = 1;
2169 } else {
2170 {
2171#line 1331
2172 errorFn();
2173 }
2174 }
2175 }
2176#line 1337
2177 if (myStatus >= 0) {
2178 {
2179#line 1339
2180 HpCdrProcessLastSession(Irp__AssociatedIrp__SystemBuffer);
2181 }
2182 }
2183#line 1344
2184 return (myStatus);
2185}
2186}
2187#line 1347 "cdaudio_simpl1.cil.c"
2188int CdAudioHPCdrDeviceControl(int DeviceObject , int Irp )
2189{ int currentIrpStack__Parameters__DeviceIoControl__IoControlCode ;
2190 int deviceExtension__TargetDeviceObject ;
2191 int irpSp__Control ;
2192 int tmp ;
2193 int tmp___0 ;
2194 int __cil_tmp8 ;
2195 int __cil_tmp9 ;
2196 int __cil_tmp10 ;
2197 int __cil_tmp11 ;
2198 int __cil_tmp12 ;
2199
2200 {
2201 {
2202#line 1355
2203 __cil_tmp8 = 56;
2204#line 1355
2205 __cil_tmp9 = 16384;
2206#line 1355
2207 __cil_tmp10 = 131072;
2208#line 1355
2209 __cil_tmp11 = 147456;
2210#line 1355
2211 __cil_tmp12 = 147512;
2212#line 1355
2213 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp12) {
2214#line 1356
2215 if (s != NP) {
2216 {
2217#line 1358
2218 errorFn();
2219 }
2220 } else {
2221#line 1361
2222 if (compRegistered != 0) {
2223 {
2224#line 1363
2225 errorFn();
2226 }
2227 } else {
2228#line 1366
2229 compRegistered = 1;
2230#line 1367
2231 routine = 0;
2232 }
2233 }
2234 {
2235#line 1371
2236 irpSp__Control = 224;
2237#line 1375
2238 tmp = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
2239 }
2240#line 1377
2241 return (tmp);
2242 } else {
2243 {
2244#line 1380
2245 tmp___0 = CdAudioSendToNextDriver(DeviceObject, Irp);
2246 }
2247#line 1382
2248 return (tmp___0);
2249 }
2250 }
2251#line 1384
2252 return (-1073741823);
2253}
2254}
2255#line 1387 "cdaudio_simpl1.cil.c"
2256int CdAudioForwardIrpSynchronous(int DeviceObject , int Irp )
2257{ int deviceExtension__TargetDeviceObject ;
2258 int event ;
2259 int status ;
2260 int irpSp__Control ;
2261
2262 {
2263#line 1394
2264 if (s != NP) {
2265 {
2266#line 1396
2267 errorFn();
2268 }
2269 } else {
2270#line 1399
2271 if (compRegistered != 0) {
2272 {
2273#line 1401
2274 errorFn();
2275 }
2276 } else {
2277#line 1404
2278 compRegistered = 1;
2279#line 1405
2280 routine = 1;
2281 }
2282 }
2283 {
2284#line 1409
2285 irpSp__Control = 224;
2286#line 1413
2287 status = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
2288#line 1414
2289 status = 259;
2290 }
2291#line 1416
2292 if (status) {
2293 {
2294#line 1418
2295 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
2296#line 1419
2297 status = myStatus;
2298 }
2299 }
2300#line 1424
2301 return (status);
2302}
2303}
2304#line 1427 "cdaudio_simpl1.cil.c"
2305void CdAudioUnload(int DriverObject )
2306{
2307
2308 {
2309#line 1431
2310 return;
2311}
2312}
2313#line 1434 "cdaudio_simpl1.cil.c"
2314int CdAudioPower(int DeviceObject , int Irp )
2315{ int Irp__CurrentLocation ;
2316 int Irp__Tail__Overlay__CurrentStackLocation ;
2317 int deviceExtension__TargetDeviceObject ;
2318 int tmp ;
2319
2320 {
2321#line 1441
2322 if (s == NP) {
2323#line 1442
2324 s = SKIP1;
2325 } else {
2326 {
2327#line 1445
2328 errorFn();
2329 }
2330 }
2331 {
2332#line 1449
2333 Irp__CurrentLocation ++;
2334#line 1450
2335 Irp__Tail__Overlay__CurrentStackLocation ++;
2336#line 1451
2337 tmp = PoCallDriver(deviceExtension__TargetDeviceObject, Irp);
2338 }
2339#line 1453
2340 return (tmp);
2341}
2342}
2343#line 1456 "cdaudio_simpl1.cil.c"
2344void stub_driver_init(void)
2345{
2346
2347 {
2348#line 1460
2349 s = NP;
2350#line 1461
2351 customIrp = 0;
2352#line 1462
2353 setEventCalled = customIrp;
2354#line 1463
2355 lowerDriverReturn = setEventCalled;
2356#line 1464
2357 compRegistered = lowerDriverReturn;
2358#line 1465
2359 compFptr = compRegistered;
2360#line 1466
2361 pended = compFptr;
2362#line 1467
2363 return;
2364}
2365}
2366#line 1470 "cdaudio_simpl1.cil.c"
2367int main(void)
2368{ int pirp__IoStatus__Status ;
2369 int d ;
2370 int status ;
2371 int irp ;
2372 int we_should_unload ;
2373
2374 int irp_choice ;
2375 int devobj ;
2376 int __cil_tmp9 ;
2377
2378 {
2379 {
2380
2381 s = 0;
2382 UNLOADED = 0;
2383 NP = 0;
2384 DC = 0;
2385 SKIP1 = 0;
2386 SKIP2 = 0;
2387 MPR1 = 0;
2388 MPR3 = 0;
2389 IPC = 0;
2390 pended = 0;
2391 compFptr = 0;
2392 compRegistered = 0;
2393 lowerDriverReturn = 0;
2394 setEventCalled = 0;
2395 customIrp = 0;
2396 routine = 0;
2397 myStatus = 0;
2398 pirp = 0;
2399 Executive = 0;
2400 Suspended = 5;
2401 KernelMode = 0;
2402 DeviceUsageTypePaging = 1;
2403
2404
2405#line 1482
2406 pirp = irp;
2407#line 1483
2408 _BLAST_init();
2409 }
2410#line 1485
2411 if (status >= 0) {
2412#line 1486
2413 s = NP;
2414#line 1487
2415 customIrp = 0;
2416#line 1488
2417 setEventCalled = customIrp;
2418#line 1489
2419 lowerDriverReturn = setEventCalled;
2420#line 1490
2421 compRegistered = lowerDriverReturn;
2422#line 1491
2423 compFptr = compRegistered;
2424#line 1492
2425 pended = compFptr;
2426#line 1493
2427 pirp__IoStatus__Status = 0;
2428#line 1494
2429 myStatus = 0;
2430#line 1495
2431 if (irp_choice == 0) {
2432#line 1496
2433 pirp__IoStatus__Status = -1073741637;
2434#line 1497
2435 myStatus = -1073741637;
2436 }
2437 {
2438#line 1502
2439 stub_driver_init();
2440 }
2441 {
2442#line 1504
2443#line 1504
2444 if (status < 0) {
2445#line 1505
2446 return (-1);
2447 }
2448 }
2449#line 1509
2450 int tmp_ndt_1;
2451 tmp_ndt_1 = __VERIFIER_nondet_int();
2452 if (tmp_ndt_1 == 2) {
2453 goto switch_5_2;
2454 } else {
2455#line 1512
2456 int tmp_ndt_2;
2457 tmp_ndt_2 = __VERIFIER_nondet_int();
2458 if (tmp_ndt_2 == 3) {
2459 goto switch_5_3;
2460 } else {
2461#line 1515
2462 int tmp_ndt_3;
2463 tmp_ndt_3 = __VERIFIER_nondet_int();
2464 if (tmp_ndt_3 == 4) {
2465 goto switch_5_4;
2466 } else {
2467 goto switch_5_default;
2468#line 1520
2469 if (0) {
2470 switch_5_2:
2471 {
2472#line 1523
2473 status = CdAudioDeviceControl(devobj, pirp);
2474 }
2475 goto switch_5_break;
2476 switch_5_3:
2477 {
2478#line 1528
2479 status = CdAudioPnp(devobj, pirp);
2480 }
2481 goto switch_5_break;
2482 switch_5_4:
2483 {
2484#line 1533
2485 status = CdAudioPower(devobj, pirp);
2486 }
2487 goto switch_5_break;
2488 switch_5_default: ;
2489#line 1537
2490 return (-1);
2491 } else {
2492 switch_5_break: ;
2493 }
2494 }
2495 }
2496 }
2497#line 1545
2498 if (we_should_unload) {
2499 {
2500#line 1547
2501 CdAudioUnload(d);
2502 }
2503 }
2504 }
2505#line 1555
2506 if (pended == 1) {
2507#line 1556
2508 if (s == NP) {
2509#line 1557
2510 s = NP;
2511 } else {
2512 goto _L___2;
2513 }
2514 } else {
2515 _L___2:
2516#line 1563
2517 if (pended == 1) {
2518#line 1564
2519 if (s == MPR3) {
2520#line 1565
2521 s = MPR3;
2522 } else {
2523 goto _L___1;
2524 }
2525 } else {
2526 _L___1:
2527#line 1571
2528 if (s != UNLOADED) {
2529#line 1574
2530 if (status != -1) {
2531#line 1577
2532 if (s != SKIP2) {
2533#line 1578
2534 if (s != IPC) {
2535#line 1579
2536 if (s != DC) {
2537 {
2538#line 1581
2539 errorFn();
2540 }
2541 } else {
2542 goto _L___0;
2543 }
2544 } else {
2545 goto _L___0;
2546 }
2547 } else {
2548 _L___0:
2549#line 1591
2550 if (pended != 1) {
2551#line 1594
2552 if (s == DC) {
2553#line 1595
2554 if (status == 259) {
2555 {
2556#line 1597
2557 errorFn();
2558 }
2559 }
2560 } else {
2561#line 1603
2562 if (status != lowerDriverReturn) {
2563 {
2564#line 1605
2565 errorFn();
2566 }
2567 }
2568 }
2569 }
2570 }
2571 }
2572 }
2573 }
2574 }
2575#line 1617
2576 return (status);
2577}
2578}
2579#line 1620 "cdaudio_simpl1.cil.c"
2580void stubMoreProcessingRequired(void)
2581{
2582
2583 {
2584#line 1624
2585 if (s == NP) {
2586#line 1625
2587 s = MPR1;
2588 } else {
2589 {
2590#line 1628
2591 errorFn();
2592 }
2593 }
2594#line 1631
2595 return;
2596}
2597}
2598#line 1634 "cdaudio_simpl1.cil.c"
2599int IofCallDriver(int DeviceObject , int Irp )
2600{ int Irp__PendingReturned ;
2601
2602 int returnVal2 ;
2603 int compRetStatus ;
2604 int lcontext ;
2605 unsigned long __cil_tmp8 ;
2606
2607 {
2608#line 1642
2609 if (compRegistered) {
2610#line 1643
2611 if (routine == 0) {
2612 {
2613#line 1645
2614 compRetStatus = HPCdrCompletion(DeviceObject, Irp, lcontext);
2615 }
2616 } else {
2617#line 1648
2618 if (routine == 1) {
2619 {
2620#line 1650
2621 compRetStatus = CdAudioSignalCompletion(DeviceObject, Irp, lcontext);
2622 }
2623 }
2624 }
2625 {
2626#line 1656
2627 __cil_tmp8 = (unsigned long )compRetStatus;
2628#line 1656
2629 if (__cil_tmp8 == -1073741802) {
2630 {
2631#line 1658
2632 stubMoreProcessingRequired();
2633 }
2634 }
2635 }
2636 }
2637#line 1666
2638 if (Irp__PendingReturned) {
2639#line 1667
2640 returnVal2 = 259;
2641 } else {
2642#line 1669
2643 int tmp_ndt_5;
2644 tmp_ndt_5 = __VERIFIER_nondet_int();
2645 if (tmp_ndt_5 == 0) {
2646 goto switch_6_0;
2647 } else {
2648#line 1672
2649 int tmp_ndt_6;
2650 tmp_ndt_6 = __VERIFIER_nondet_int();
2651 if (tmp_ndt_6 == 1) {
2652 goto switch_6_1;
2653 } else {
2654 goto switch_6_default;
2655#line 1677
2656 if (0) {
2657 switch_6_0:
2658#line 1679
2659 returnVal2 = 0;
2660 goto switch_6_break;
2661 switch_6_1:
2662#line 1682
2663 returnVal2 = -1073741823;
2664 goto switch_6_break;
2665 switch_6_default:
2666#line 1685
2667 returnVal2 = 259;
2668 goto switch_6_break;
2669 } else {
2670 switch_6_break: ;
2671 }
2672 }
2673 }
2674 }
2675#line 1694
2676 if (s == NP) {
2677#line 1695
2678 s = IPC;
2679#line 1696
2680 lowerDriverReturn = returnVal2;
2681 } else {
2682#line 1698
2683 if (s == MPR1) {
2684#line 1699
2685 if (returnVal2 == 259) {
2686#line 1700
2687 s = MPR3;
2688#line 1701
2689 lowerDriverReturn = returnVal2;
2690 } else {
2691#line 1703
2692 s = NP;
2693#line 1704
2694 lowerDriverReturn = returnVal2;
2695 }
2696 } else {
2697#line 1707
2698 if (s == SKIP1) {
2699#line 1708
2700 s = SKIP2;
2701#line 1709
2702 lowerDriverReturn = returnVal2;
2703 } else {
2704 {
2705#line 1712
2706 errorFn();
2707 }
2708 }
2709 }
2710 }
2711#line 1717
2712 return (returnVal2);
2713}
2714}
2715#line 1720 "cdaudio_simpl1.cil.c"
2716void IofCompleteRequest(int Irp , int PriorityBoost )
2717{
2718
2719 {
2720#line 1724
2721 if (s == NP) {
2722#line 1725
2723 s = DC;
2724 } else {
2725 {
2726#line 1728
2727 errorFn();
2728 }
2729 }
2730#line 1731
2731 return;
2732}
2733}
2734#line 1734 "cdaudio_simpl1.cil.c"
2735int KeSetEvent(int Event , int Increment , int Wait )
2736{ int l ;
2737
2738 {
2739#line 1738
2740 setEventCalled = 1;
2741#line 1739
2742 return (l);
2743}
2744}
2745#line 1742 "cdaudio_simpl1.cil.c"
2746int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
2747 int Timeout )
2748{
2749
2750 {
2751#line 1747
2752 if (s == MPR3) {
2753#line 1748
2754 if (setEventCalled == 1) {
2755#line 1749
2756 s = NP;
2757#line 1750
2758 setEventCalled = 0;
2759 } else {
2760 goto _L;
2761 }
2762 } else {
2763 _L:
2764#line 1756
2765 if (customIrp == 1) {
2766#line 1757
2767 s = NP;
2768#line 1758
2769 customIrp = 0;
2770 } else {
2771#line 1760
2772 if (s == MPR3) {
2773 {
2774#line 1762
2775 errorFn();
2776 }
2777 }
2778 }
2779 }
2780#line 1769
2781 int tmp_ndt_7;
2782 tmp_ndt_7 = __VERIFIER_nondet_int();
2783 if (tmp_ndt_7 == 0) {
2784 goto switch_7_0;
2785 } else {
2786 goto switch_7_default;
2787#line 1774
2788 if (0) {
2789 switch_7_0: ;
2790#line 1776
2791 return (0);
2792 switch_7_default: ;
2793#line 1778
2794 return (-1073741823);
2795 } else {
2796
2797 }
2798 }
2799}
2800}
2801#line 1786 "cdaudio_simpl1.cil.c"
2802int PoCallDriver(int DeviceObject , int Irp )
2803{
2804 int compRetStatus ;
2805 int returnVal ;
2806 int lcontext ;
2807 unsigned long __cil_tmp7 ;
2808 long __cil_tmp8 ;
2809
2810 {
2811#line 1793
2812 if (compRegistered) {
2813#line 1794
2814 if (routine == 0) {
2815 {
2816#line 1796
2817 compRetStatus = HPCdrCompletion(DeviceObject, Irp, lcontext);
2818 }
2819 } else {
2820#line 1799
2821 if (routine == 1) {
2822 {
2823#line 1801
2824 compRetStatus = CdAudioSignalCompletion(DeviceObject, Irp, lcontext);
2825 }
2826 }
2827 }
2828 {
2829#line 1807
2830 __cil_tmp7 = (unsigned long )compRetStatus;
2831#line 1807
2832 if (__cil_tmp7 == -1073741802) {
2833 {
2834#line 1809
2835 stubMoreProcessingRequired();
2836 }
2837 }
2838 }
2839 }
2840#line 1817
2841 int tmp_ndt_8;
2842 tmp_ndt_8 = __VERIFIER_nondet_int();
2843 if (tmp_ndt_8 == 0) {
2844 goto switch_8_0;
2845 } else {
2846#line 1820
2847 int tmp_ndt_9;
2848 tmp_ndt_9 = __VERIFIER_nondet_int();
2849 if (tmp_ndt_9 == 1) {
2850 goto switch_8_1;
2851 } else {
2852 goto switch_8_default;
2853#line 1825
2854 if (0) {
2855 switch_8_0:
2856#line 1827
2857 returnVal = 0;
2858 goto switch_8_break;
2859 switch_8_1:
2860#line 1830
2861 returnVal = -1073741823;
2862 goto switch_8_break;
2863 switch_8_default:
2864#line 1833
2865 returnVal = 259;
2866 goto switch_8_break;
2867 } else {
2868 switch_8_break: ;
2869 }
2870 }
2871 }
2872#line 1841
2873 if (s == NP) {
2874#line 1842
2875 s = IPC;
2876#line 1843
2877 lowerDriverReturn = returnVal;
2878 } else {
2879#line 1845
2880 if (s == MPR1) {
2881 {
2882#line 1846
2883 __cil_tmp8 = (long )returnVal;
2884#line 1846
2885 if (__cil_tmp8 == 259L) {
2886#line 1847
2887 s = MPR3;
2888#line 1848
2889 lowerDriverReturn = returnVal;
2890 } else {
2891#line 1850
2892 s = NP;
2893#line 1851
2894 lowerDriverReturn = returnVal;
2895 }
2896 }
2897 } else {
2898#line 1854
2899 if (s == SKIP1) {
2900#line 1855
2901 s = SKIP2;
2902#line 1856
2903 lowerDriverReturn = returnVal;
2904 } else {
2905 {
2906#line 1859
2907 errorFn();
2908 }
2909 }
2910 }
2911 }
2912#line 1864
2913 return (returnVal);
2914}
2915}
2916#line 1867 "cdaudio_simpl1.cil.c"
2917int ZwClose(int Handle )
2918{
2919
2920 {
2921#line 1871
2922 int tmp_ndt_10;
2923 tmp_ndt_10 = __VERIFIER_nondet_int();
2924 if (tmp_ndt_10 == 0) {
2925 goto switch_9_0;
2926 } else {
2927 goto switch_9_default;
2928#line 1876
2929 if (0) {
2930 switch_9_0: ;
2931#line 1878
2932 return (0);
2933 switch_9_default: ;
2934#line 1880
2935 return (-1073741823);
2936 } else {
2937
2938 }
2939 }
2940}
2941}