Context Navigation

cdaudio_simpl1_false-unreach-call_true-termination.cil.c

main

Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c

Property mode set to 100644

File size: 71.8 KB

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

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: CIVL/mods/dev.civl.abc/examples/svcomp/cdaudio_simpl1_false-unreach-call_true-termination.cil.c

Download in other formats: