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

Rev	Line
[aad342c]	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: