5void IofCompleteRequest(int Irp , int PriorityBoost );
6int __VERIFIER_nondet_int() ;
7int s ;
8int UNLOADED ;
9int NP ;
10int DC ;
11int SKIP1 ;
12int SKIP2 ;
13int MPR1 ;
14int MPR3 ;
15int IPC ;
16int pended ;
17int compFptr ;
18int compRegistered ;
19int lowerDriverReturn ;
20int setEventCalled ;
21int customIrp ;
22int routine ;
23int myStatus ;
24int pirp ;
25int Executive ;
26int Suspended ;
27int KernelMode ;
28int DeviceUsageTypePaging ;
29
30void errorFn(void)
31{
32
33 {
34 goto ERROR;
35 ERROR:
36#line 60
37 return;
38}
39}
40#line 63 "cdaudio_simpl1.cil.c"
41void _BLAST_init(void)
42{
43
44 {
45#line 67