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