1int __VERIFIER_nondet_int() ;
2int s ;
3int UNLOADED ;
4int NP ;
5int DC ;
6int SKIP1 ;
7int SKIP2 ;
8int MPR1 ;
9int MPR3 ;
10int IPC ;
11int pended ;
12int compFptr ;
13int compRegistered ;
14int lowerDriverReturn ;
15int setEventCalled ;
16int customIrp ;
17int myStatus ;
18int routine ;
19int pirp ;
20int Executive ;
21int KernelMode ;
22
23void errorFn(void)
24{
25
26 {
27 goto ERROR;
28 ERROR:
29#line 58
30 return;
31}
32}
33#line 61 "diskperf_simpl1.cil.c"
34void _BLAST_init(void)
35{
36
37 {
38#line 65
39 UNLOADED = 0;
40#line 66
41 NP = 1;
42#line 67
43 DC = 2;
44#line 68
45 SKIP1 = 3;
46#line 69
47 SKIP2 = 4;
48#line 70
49 MPR1 = 5;
50#line 71
51 MPR3 = 6;
52#line 72
53 IPC = 7;
54#line 73
55 s = UNLOADED;
56#line 74
57 pended = 0;
58#line 75
59 compFptr = 0;
60#line 76
61 compRegistered = 0;
62#line 77
63 lowerDriverReturn = 0;
64#line 78
65 setEventCalled = 0;
66#line 79
67 customIrp = 0;
68#line 80
69 return;
70}
71}
72#line 83 "diskperf_simpl1.cil.c"
73void DiskPerfSyncFilterWithTarget(int FilterDevice , int TargetDevice )
74{ int FilterDevice__Flags ;
75 int TargetDevice__Characteristics ;
76 int FilterDevice__Characteristics ;
77 int propFlags ;
78
79 {
80#line 90
81
82#line 91
83
84#line 92
85
86#line 93
87
88#line 94
89 return;
90}
91}
92#line 97 "diskperf_simpl1.cil.c"
93int DiskPerfDispatchPnp(int DeviceObject , int Irp )
94{ int Irp__Tail__Overlay__CurrentStackLocation ;
95 int irpSp__MinorFunction ;
96 int irpSp ;
97 int status ;
98 int tmp ;
99
100 {
101#line 105
102 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
103#line 106
104 if (irpSp__MinorFunction == 0) {
105 goto switch_0_0;
106 } else {
107#line 109
108 if (irpSp__MinorFunction == 2) {
109 goto switch_0_2;
110 } else {
111 goto switch_0_default;
112#line 114
113 if (0) {
114 switch_0_0:
115 {
116#line 117
117 status = DiskPerfStartDevice(DeviceObject, Irp);
118 }
119 goto switch_0_break;
120 switch_0_2:
121 {
122#line 122
123 status = DiskPerfRemoveDevice(DeviceObject, Irp);
124 }
125 goto switch_0_break;
126 switch_0_default:
127 {
128#line 127
129 tmp = DiskPerfSendToNextDriver(DeviceObject, Irp);
130 }
131#line 129
132 return (tmp);
133 } else {
134 switch_0_break: ;
135 }
136 }
137 }
138#line 136
139 return (status);
140}
141}
142#line 139 "diskperf_simpl1.cil.c"
143int DiskPerfIrpCompletion(int DeviceObject , int Irp , int Context )
144{ int Event ;
145
146 {
147 {
148#line 144
149 Event = Context;
150#line 145
151 KeSetEvent(Event, 0, 0);
152 }
153#line 147
154 return (-1073741802);
155}
156}
157#line 150 "diskperf_simpl1.cil.c"
158int DiskPerfStartDevice(int DeviceObject , int Irp )
159{ int DeviceObject__DeviceExtension ;
160 int deviceExtension__TargetDeviceObject ;
161 int Irp__IoStatus__Status ;
162 int deviceExtension ;
163 int status ;
164
165 {
166 {
167#line 159
168 deviceExtension = DeviceObject__DeviceExtension;
169#line 160
170 status = DiskPerfForwardIrpSynchronous(DeviceObject, Irp);
171#line 161
172 DiskPerfSyncFilterWithTarget(DeviceObject, deviceExtension__TargetDeviceObject);
173#line 162
174 DiskPerfRegisterDevice(DeviceObject);
175#line 163
176 Irp__IoStatus__Status = status;
177#line 164
178 myStatus = status;
179#line 165
180 IofCompleteRequest(Irp, 0);
181 }
182#line 167
183 return (status);
184}
185}
186#line 170 "diskperf_simpl1.cil.c"
187int DiskPerfRemoveDevice(int DeviceObject , int Irp )
188{ int DeviceObject__DeviceExtension ;
189 int deviceExtension__WmilibContext ;
190 int Irp__IoStatus__Status ;
191 int status ;
192 int deviceExtension ;
193 int wmilibContext ;
194
195 {
196 {
197#line 180
198 deviceExtension = DeviceObject__DeviceExtension;
199#line 181
200 wmilibContext = deviceExtension__WmilibContext;
201#line 182
202 status = DiskPerfForwardIrpSynchronous(DeviceObject, Irp);
203#line 183
204 Irp__IoStatus__Status = status;
205#line 184
206 myStatus = status;
207#line 185
208 IofCompleteRequest(Irp, 0);
209 }
210#line 187
211 return (status);
212}
213}
214#line 190 "diskperf_simpl1.cil.c"
215int DiskPerfSendToNextDriver(int DeviceObject , int Irp )
216{ int Irp__CurrentLocation ;
217 int Irp__Tail__Overlay__CurrentStackLocation ;
218 int DeviceObject__DeviceExtension ;
219 int deviceExtension__TargetDeviceObject ;
220 int deviceExtension ;
221 int tmp ;
222
223 {
224#line 199
225 if (s == NP) {
226#line 200
227 s = SKIP1;
228 } else {
229 {
230#line 203
231 errorFn();
232 }
233 }
234 {
235#line 207
236 Irp__CurrentLocation ++;
237#line 208
238 Irp__Tail__Overlay__CurrentStackLocation ++;
239#line 209
240 deviceExtension = DeviceObject__DeviceExtension;
241#line 210
242 tmp = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
243 }
244#line 212
245 return (tmp);
246}
247}
248#line 215 "diskperf_simpl1.cil.c"
249int DiskPerfDispatchPower(int DeviceObject , int Irp )
250{ int Irp__CurrentLocation ;
251 int Irp__Tail__Overlay__CurrentStackLocation ;
252 int DeviceObject__DeviceExtension ;
253 int deviceExtension__TargetDeviceObject ;
254 int deviceExtension ;
255 int tmp ;
256
257 {
258#line 224
259 if (s == NP) {
260#line 225
261 s = SKIP1;
262 } else {
263 {
264#line 228
265 errorFn();
266 }
267 }
268 {
269#line 232
270 Irp__CurrentLocation ++;
271#line 233
272 Irp__Tail__Overlay__CurrentStackLocation ++;
273#line 234
274 deviceExtension = DeviceObject__DeviceExtension;
275#line 235
276 tmp = PoCallDriver(deviceExtension__TargetDeviceObject, Irp);
277 }
278#line 237
279 return (tmp);
280}
281}
282#line 240 "diskperf_simpl1.cil.c"
283int DiskPerfForwardIrpSynchronous(int DeviceObject , int Irp )
284{ int Irp__Tail__Overlay__CurrentStackLocation ;
285 int DeviceObject__DeviceExtension ;
286 int deviceExtension__TargetDeviceObject ;
287 int deviceExtension ;
288 int event ;
289 int status ;
290 int nextIrpSp__Control ;
291 int irpSp ;
292 int nextIrpSp ;
293 int irpSp__Context ;
294 int irpSp__Control ;
295 int irpSp___0 ;
296 long __cil_tmp15 ;
297
298 {
299#line 255
300 deviceExtension = DeviceObject__DeviceExtension;
301#line 256
302 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
303#line 257
304 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
305#line 258
306 nextIrpSp__Control = 0;
307#line 259
308 if (s != NP) {
309 {
310#line 261
311 errorFn();
312 }
313 } else {
314#line 264
315 if (compRegistered != 0) {
316 {
317#line 266
318 errorFn();
319 }
320 } else {
321#line 269
322 compRegistered = 1;
323#line 270
324 routine = 0;
325 }
326 }
327 {
328#line 274
329 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation - 1;
330#line 275
331 irpSp__Context = event;
332#line 276
333 irpSp__Control = 224;
334#line 280
335 status = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
336 }
337 {
338#line 282
339 __cil_tmp15 = (long )status;
340#line 282
341 if (__cil_tmp15 == 259L) {
342 {
343#line 284
344 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
345#line 285
346 status = myStatus;
347 }
348 }
349 }
350#line 290
351 return (status);
352}
353}
354#line 293 "diskperf_simpl1.cil.c"
355int DiskPerfCreate(int DeviceObject , int Irp )
356{
357
358 {
359 {
360#line 298
361 myStatus = 0;
362#line 299
363 IofCompleteRequest(Irp, 0);
364 }
365#line 301
366 return (0);
367}
368}
369#line 304 "diskperf_simpl1.cil.c"
370int DiskPerfIoCompletion(int DeviceObject , int Irp , int Context )
371{ int irpStack__MajorFunction ;
372 int partitionCounters__BytesRead__QuadPart ;
373 int Irp__IoStatus__Information ;
374 int partitionCounters__ReadCount ;
375 int partitionCounters__ReadTime__QuadPart ;
376 int difference__QuadPart ;
377 int partitionCounters__BytesWritten__QuadPart ;
378 int partitionCounters__WriteCount ;
379 int partitionCounters__WriteTime__QuadPart ;
380 int Irp__Flags ;
381 int partitionCounters__SplitCount ;
382 int Irp__PendingReturned ;
383 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
384 int partitionCounters ;
385 int queueLen ;
386
387 {
388#line 322
389 if (partitionCounters == 0) {
390#line 323
391 return (0);
392 }
393#line 327
394 if (queueLen < 0) {
395
396 }
397#line 332
398 if (queueLen == 0) {
399
400 }
401#line 337
402 if (irpStack__MajorFunction == 3) {
403#line 338
404 partitionCounters__BytesRead__QuadPart += Irp__IoStatus__Information;
405#line 339
406 partitionCounters__ReadCount ++;
407#line 340
408 partitionCounters__ReadTime__QuadPart += difference__QuadPart;
409 } else {
410#line 342
411 partitionCounters__BytesWritten__QuadPart += Irp__IoStatus__Information;
412#line 343
413 partitionCounters__WriteCount ++;
414#line 344
415 partitionCounters__WriteTime__QuadPart += difference__QuadPart;
416 }
417#line 346
418 if (Irp__Flags != 8) {
419#line 347
420 partitionCounters__SplitCount ++;
421 }
422 else {
423 }
424#line 351
425 if (Irp__PendingReturned) {
426#line 352
427 if (pended == 0) {
428#line 353
429 pended = 1;
430 } else {
431 {
432#line 356
433 errorFn();
434 }
435 }
436#line 359
437
438 }
439#line 363
440 return (0);
441}
442}
443#line 366 "diskperf_simpl1.cil.c"
444int DiskPerfDeviceControl(int DeviceObject , int Irp )
445{ int Irp__CurrentLocation ;
446 int Irp__Tail__Overlay__CurrentStackLocation ;
447 int DeviceObject__DeviceExtension ;
448 int deviceExtension__TargetDeviceObject ;
449 int currentIrpStack__Parameters__DeviceIoControl__IoControlCode ;
450 int currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength ;
451 int sizeof__DISK_PERFORMANCE ;
452 int Irp__IoStatus__Information ;
453 int deviceExtension__DiskCounters ;
454 int Irp__AssociatedIrp__SystemBuffer ;
455 int deviceExtension__Processors ;
456 int totalCounters__QueueDepth ;
457 int deviceExtension__QueueDepth ;
458 int Irp__IoStatus__Status ;
459 int deviceExtension ;
460 int currentIrpStack ;
461 int status ;
462 int i ;
463 int totalCounters ;
464 int diskCounters ;
465 int tmp ;
466 int __cil_tmp24 ;
467 int __cil_tmp25 ;
468 int __cil_tmp26 ;
469
470 {
471#line 390
472 deviceExtension = DeviceObject__DeviceExtension;
473#line 391
474 currentIrpStack = Irp__Tail__Overlay__CurrentStackLocation;
475 {
476#line 392
477 __cil_tmp24 = 32;
478#line 392
479 __cil_tmp25 = 458752;
480#line 392
481 __cil_tmp26 = 458784;
482#line 392
483 if (currentIrpStack__Parameters__DeviceIoControl__IoControlCode == __cil_tmp26) {
484#line 393
485 if (currentIrpStack__Parameters__DeviceIoControl__OutputBufferLength < sizeof__DISK_PERFORMANCE) {
486#line 394
487 status = -1073741789;
488#line 395
489 Irp__IoStatus__Information = 0;
490 } else {
491#line 397
492 diskCounters = deviceExtension__DiskCounters;
493#line 398
494 if (diskCounters == 0) {
495 {
496#line 400
497 Irp__IoStatus__Status = -1073741823;
498#line 401
499 myStatus = -1073741823;
500#line 402
501 IofCompleteRequest(Irp, 0);
502 }
503#line 404
504 return (-1073741823);
505 }
506#line 408
507 totalCounters = Irp__AssociatedIrp__SystemBuffer;
508#line 409
509 i = 0;
510 {
511#line 411
512 while (1) {
513 while_0_continue: ;
514
515#line 413
516 if (i >= deviceExtension__Processors) {
517 goto while_1_break;
518 }
519#line 418
520 i ++;
521 }
522 while_0_break: ;
523 }
524 while_1_break:
525#line 422
526 totalCounters__QueueDepth = deviceExtension__QueueDepth;
527#line 423
528 status = 0;
529#line 424
530 Irp__IoStatus__Information = sizeof__DISK_PERFORMANCE;
531 }
532 {
533#line 427
534 Irp__IoStatus__Status = status;
535#line 428
536 myStatus = status;
537#line 429
538 IofCompleteRequest(Irp, 0);
539 }
540#line 431
541 return (status);
542 } else {
543 {
544#line 434
545 Irp__CurrentLocation ++;
546#line 435
547 Irp__Tail__Overlay__CurrentStackLocation ++;
548#line 436
549 tmp = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
550 }
551#line 438
552 return (tmp);
553 }
554 }
555}
556}
557#line 442 "diskperf_simpl1.cil.c"
558int DiskPerfShutdownFlush(int DeviceObject , int Irp )
559{ int DeviceObject__DeviceExtension ;
560 int Irp__CurrentLocation ;
561 int Irp__Tail__Overlay__CurrentStackLocation ;
562 int deviceExtension__TargetDeviceObject ;
563 int deviceExtension ;
564 int tmp ;
565
566 {
567 {
568#line 452
569 deviceExtension = DeviceObject__DeviceExtension;
570#line 453
571 Irp__CurrentLocation ++;
572#line 454
573 Irp__Tail__Overlay__CurrentStackLocation ++;
574#line 455
575 tmp = IofCallDriver(deviceExtension__TargetDeviceObject, Irp);
576 }
577#line 457
578 return (tmp);
579}
580}
581#line 460 "diskperf_simpl1.cil.c"
582void DiskPerfUnload(int DriverObject )
583{
584
585 {
586#line 464
587 return;
588}
589}
590#line 467 "diskperf_simpl1.cil.c"
591int DiskPerfRegisterDevice(int DeviceObject )
592{ int DeviceObject__DeviceExtension ;
593 int deviceExtension__TargetDeviceObject ;
594 int sizeof__number ;
595 int ioStatus__Status ;
596 int sizeof__VOLUME_NUMBER ;
597 int volumeNumber__VolumeManagerName__0 ;
598 int status ;
599 int ioStatus ;
600 int event ;
601 int deviceExtension ;
602 int irp ;
603 int number ;
604 int registrationFlag ;
605 int sizeof__MOUNTDEV_NAME ;
606 int output__NameLength ;
607 int outputSize ;
608 int output ;
609 int volumeNumber ;
610 int __cil_tmp20 ;
611 int __cil_tmp21 ;
612 int __cil_tmp22 ;
613 long __cil_tmp23 ;
614 int __cil_tmp24 ;
615 int __cil_tmp25 ;
616 int __cil_tmp26 ;
617 long __cil_tmp27 ;
618 unsigned long __cil_tmp28 ;
619 int __cil_tmp29 ;
620 int __cil_tmp30 ;
621 int __cil_tmp31 ;
622 long __cil_tmp32 ;
623 int __cil_tmp33 ;
624 int __cil_tmp34 ;
625 int __cil_tmp35 ;
626 int __cil_tmp36 ;
627 long __cil_tmp37 ;
628 int __cil_tmp38 ;
629 int __cil_tmp39 ;
630
631 {
632 {
633#line 489
634 registrationFlag = 0;
635#line 490
636 deviceExtension = DeviceObject__DeviceExtension;
637#line 491
638 __cil_tmp20 = 4224;
639#line 491
640 __cil_tmp21 = 2949120;
641#line 491
642 __cil_tmp22 = 2953344;
643#line 491
644 irp = IoBuildDeviceIoControlRequest(__cil_tmp22, deviceExtension__TargetDeviceObject,
645 0, 0, number, sizeof__number, 0, event, ioStatus);
646 }
647#line 494
648 if (! irp) {
649#line 495
650 return (-1073741670);
651 }
652 {
653#line 500
654 status = IofCallDriver(deviceExtension__TargetDeviceObject, irp);
655 }
656 {
657#line 502
658 __cil_tmp23 = (long )status;
659#line 502
660 if (__cil_tmp23 == 259L) {
661 {
662#line 504
663 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
664#line 505
665 status = ioStatus__Status;
666 }
667 }
668 }
669#line 510
670 if (status < 0) {
671#line 513
672 outputSize = sizeof__MOUNTDEV_NAME;
673#line 514
674 if (! output) {
675#line 515
676 return (-1073741670);
677 }
678 {
679#line 520
680 __cil_tmp24 = 8;
681#line 520
682 __cil_tmp25 = 5046272;
683#line 520
684 __cil_tmp26 = 5046280;
685#line 520
686 irp = IoBuildDeviceIoControlRequest(__cil_tmp26, deviceExtension__TargetDeviceObject,
687 0, 0, output, outputSize, 0, event, ioStatus);
688 }
689#line 523
690 if (! irp) {
691#line 524
692 return (-1073741670);
693 }
694 {
695#line 529
696 status = IofCallDriver(deviceExtension__TargetDeviceObject, irp);
697 }
698 {
699#line 531
700 __cil_tmp27 = (long )status;
701#line 531
702 if (__cil_tmp27 == 259L) {
703 {
704#line 533
705 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
706#line 534
707 status = ioStatus__Status;
708 }
709 }
710 }
711 {
712#line 539
713 __cil_tmp28 = (unsigned long )status;
714#line 539
715 if (__cil_tmp28 == -2147483643) {
716#line 540
717 outputSize = sizeof__MOUNTDEV_NAME + output__NameLength;
718#line 541
719 if (! output) {
720#line 542
721 return (-1073741670);
722 }
723 {
724#line 547
725 __cil_tmp29 = 8;
726#line 547
727 __cil_tmp30 = 5046272;
728#line 547
729 __cil_tmp31 = 5046280;
730#line 547
731 irp = IoBuildDeviceIoControlRequest(__cil_tmp31, deviceExtension__TargetDeviceObject,
732 0, 0, output, outputSize, 0, event, ioStatus);
733 }
734#line 550
735 if (! irp) {
736#line 551
737 return (-1073741670);
738 }
739 {
740#line 556
741 status = IofCallDriver(deviceExtension__TargetDeviceObject, irp);
742 }
743 {
744#line 558
745 __cil_tmp32 = (long )status;
746#line 558
747 if (__cil_tmp32 == 259L) {
748 {
749#line 560
750 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
751#line 561
752 status = ioStatus__Status;
753 }
754 }
755 }
756 }
757 }
758 {
759#line 569
760 if (status < 0) {
761#line 570
762 return (status);
763 }
764 }
765 {
766#line 575
767 __cil_tmp34 = 28;
768#line 575
769 __cil_tmp35 = 5636096;
770#line 575
771 __cil_tmp36 = 5636124;
772#line 575
773 irp = IoBuildDeviceIoControlRequest(__cil_tmp36, deviceExtension__TargetDeviceObject,
774 0, 0, volumeNumber, sizeof__VOLUME_NUMBER,
775 0, event, ioStatus);
776 }
777#line 579
778 if (! irp) {
779#line 580
780 return (-1073741670);
781 }
782 {
783#line 585
784 status = IofCallDriver(deviceExtension__TargetDeviceObject, irp);
785 }
786 {
787#line 587
788 __cil_tmp37 = (long )status;
789#line 587
790 if (__cil_tmp37 == 259L) {
791 {
792#line 589
793 KeWaitForSingleObject(event, Executive, KernelMode, 0, 0);
794#line 590
795 status = ioStatus__Status;
796 }
797 }
798 }
799 {
800#line 595
801 if (status < 0) {
802 goto _L;
803 } else {
804#line 598
805 if (volumeNumber__VolumeManagerName__0 == 0) {
806 _L:
807#line 600
808 if (status >= 0) {
809
810 }
811 }
812 }
813 }
814 }
815 {
816#line 610
817#line 610
818 if (status < 0) {
819
820 }
821 }
822#line 615
823 return (status);
824}
825}
826#line 618 "diskperf_simpl1.cil.c"
827void stub_driver_init(void)
828{
829
830 {
831#line 622
832 s = NP;
833#line 623
834 customIrp = 0;
835#line 624
836 setEventCalled = customIrp;
837#line 625
838 lowerDriverReturn = setEventCalled;
839#line 626
840 compRegistered = lowerDriverReturn;
841#line 627
842 compFptr = compRegistered;
843#line 628
844 pended = compFptr;
845#line 629
846 return;
847}
848}
849#line 632 "diskperf_simpl1.cil.c"
850int main(void)
851{ int d ;
852 int status ;
853 int we_should_unload ;
854 int irp ;
855 int pirp__IoStatus__Status ;
856
857 int irp_choice ;
858 int devobj ;
859 int __cil_tmp9 ;
860
861 s = 0;
862 UNLOADED = 0;
863 NP = 0;
864 DC = 0;
865 SKIP1 = 0;
866 SKIP2 = 0;
867 MPR1 = 0;
868 MPR3 = 0;
869 IPC = 0;
870 pended = 0;
871 compFptr = 0;
872 compRegistered = 0;
873 lowerDriverReturn = 0;
874 setEventCalled = 0;
875 customIrp = 0;
876 myStatus = 0;
877 routine = 0;
878 pirp = 0;
879 Executive = 0;
880 KernelMode = 0;
881
882 {
883 {
884#line 644
885 pirp = irp;
886#line 645
887 _BLAST_init();
888 }
889#line 647
890 if (status >= 0) {
891#line 648
892 s = NP;
893#line 649
894 customIrp = 0;
895#line 650
896 setEventCalled = customIrp;
897#line 651
898 lowerDriverReturn = setEventCalled;
899#line 652
900 compRegistered = lowerDriverReturn;
901#line 653
902 compFptr = compRegistered;
903#line 654
904 pended = compFptr;
905#line 655
906 pirp__IoStatus__Status = 0;
907#line 656
908 myStatus = 0;
909#line 657
910 if (irp_choice == 0) {
911#line 658
912 pirp__IoStatus__Status = -1073741637;
913#line 659
914 myStatus = -1073741637;
915 }
916 {
917#line 664
918 stub_driver_init();
919 }
920 {
921#line 666
922 if (status < 0) {
923#line 667
924 return (-1);
925 }
926 }
927#line 671
928 int tmp_ndt_1;
929 tmp_ndt_1 = __VERIFIER_nondet_int();
930 if (tmp_ndt_1 == 0) {
931 goto switch_2_0;
932 } else {
933#line 674
934 int tmp_ndt_2;
935 tmp_ndt_2 = __VERIFIER_nondet_int();
936 if (tmp_ndt_2 == 2) {
937 goto switch_2_2;
938 } else {
939#line 677
940 int tmp_ndt_3;
941 tmp_ndt_3 = __VERIFIER_nondet_int();
942 if (tmp_ndt_3 == 3) {
943 goto switch_2_3;
944 } else {
945#line 680
946 int tmp_ndt_4;
947 tmp_ndt_4 = __VERIFIER_nondet_int();
948 if (tmp_ndt_4 == 4) {
949 goto switch_2_4;
950 } else {
951#line 683
952 int tmp_ndt_5;
953 tmp_ndt_5 = __VERIFIER_nondet_int();
954 if (tmp_ndt_5 == 12) {
955 goto switch_2_12;
956 } else {
957 goto switch_2_default;
958#line 688
959 if (0) {
960 switch_2_0:
961 {
962#line 691
963 status = DiskPerfCreate(devobj, pirp);
964 }
965 goto switch_2_break;
966 switch_2_2:
967 {
968#line 696
969 status = DiskPerfDeviceControl(devobj, pirp);
970 }
971 goto switch_2_break;
972 switch_2_3:
973 {
974#line 701
975 status = DiskPerfDispatchPnp(devobj, pirp);
976 }
977 goto switch_2_break;
978 switch_2_4:
979 {
980#line 706
981 status = DiskPerfDispatchPower(devobj, pirp);
982 }
983 goto switch_2_break;
984 switch_2_12:
985 {
986#line 711
987 status = DiskPerfShutdownFlush(devobj, pirp);
988 }
989 goto switch_2_break;
990 switch_2_default: ;
991#line 715
992 return (-1);
993 } else {
994 switch_2_break: ;
995 }
996 }
997 }
998 }
999 }
1000 }
1001#line 725
1002 if (we_should_unload) {
1003 {
1004#line 727
1005 DiskPerfUnload(d);
1006 }
1007 }
1008 }
1009#line 735
1010 if (pended == 1) {
1011#line 736
1012 if (s == NP) {
1013#line 737
1014 s = NP;
1015 } else {
1016 goto _L___2;
1017 }
1018 } else {
1019 _L___2:
1020#line 743
1021 if (pended == 1) {
1022#line 744
1023 if (s == MPR3) {
1024#line 745
1025 s = MPR3;
1026 } else {
1027 goto _L___1;
1028 }
1029 } else {
1030 _L___1:
1031#line 751
1032 if (s != UNLOADED) {
1033#line 754
1034 if (status != -1) {
1035#line 757
1036 if (s != SKIP2) {
1037#line 758
1038 if (s != IPC) {
1039#line 759
1040 if (s != DC) {
1041 {
1042#line 761
1043 errorFn();
1044 }
1045 } else {
1046 goto _L___0;
1047 }
1048 } else {
1049 goto _L___0;
1050 }
1051 } else {
1052 _L___0:
1053#line 771
1054 if (pended == 1) {
1055#line 772
1056 if (status != 259) {
1057 {
1058#line 774
1059 errorFn();
1060 }
1061 }
1062 } else {
1063#line 780
1064 if (s == DC) {
1065#line 781
1066 if (status == 259) {
1067 {
1068#line 783
1069 errorFn();
1070 }
1071 }
1072 } else {
1073#line 789
1074 if (status != lowerDriverReturn) {
1075 {
1076#line 791
1077 errorFn();
1078 }
1079 }
1080 }
1081 }
1082 }
1083 }
1084 }
1085 }
1086 }
1087#line 803
1088 return (status);
1089}
1090}
1091#line 806 "diskperf_simpl1.cil.c"
1092int IoBuildDeviceIoControlRequest(int IoControlCode , int DeviceObject , int InputBuffer ,
1093 int InputBufferLength , int OutputBuffer , int OutputBufferLength ,
1094 int InternalDeviceIoControl , int Event , int IoStatusBlock )
1095{
1096 int malloc_ret ;
1097
1098 {
1099#line 813
1100 customIrp = 1;
1101#line 814
1102 int tmp_ndt_7;
1103 tmp_ndt_7 = __VERIFIER_nondet_int();
1104 if (tmp_ndt_7 == 0) {
1105 goto switch_3_0;
1106 } else {
1107 goto switch_3_default;
1108#line 819
1109 if (0) {
1110 switch_3_0: ;
1111#line 821
1112 return (malloc_ret);
1113 switch_3_default: ;
1114#line 823
1115 return (0);
1116 } else {
1117
1118 }
1119 }
1120}
1121}
1122#line 831 "diskperf_simpl1.cil.c"
1123void stubMoreProcessingRequired(void)
1124{
1125
1126 {
1127#line 835
1128 if (s == NP) {
1129#line 836
1130 s = MPR1;
1131 } else {
1132 {
1133#line 839
1134 errorFn();
1135 }
1136 }
1137#line 842
1138 return;
1139}
1140}
1141#line 845 "diskperf_simpl1.cil.c"
1142int IofCallDriver(int DeviceObject , int Irp )
1143{
1144 int returnVal2 ;
1145 int compRetStatus ;
1146 int lcontext ;
1147 unsigned long __cil_tmp7 ;
1148
1149 {
1150#line 852
1151 if (compRegistered) {
1152#line 853
1153 if (routine == 0) {
1154 {
1155#line 855
1156 compRetStatus = DiskPerfIrpCompletion(DeviceObject, Irp, lcontext);
1157 }
1158 } else {
1159 {
1160#line 859
1161 compRetStatus = DiskPerfIoCompletion(DeviceObject, Irp, lcontext);
1162 }
1163 }
1164 {
1165#line 862
1166 __cil_tmp7 = (unsigned long )compRetStatus;
1167#line 862
1168 if (__cil_tmp7 == -1073741802) {
1169 {
1170#line 864
1171 stubMoreProcessingRequired();
1172 }
1173 }
1174 }
1175 }
1176#line 872
1177 int tmp_ndt_8;
1178 tmp_ndt_8 = __VERIFIER_nondet_int();
1179 if (tmp_ndt_8 == 0) {
1180 goto switch_4_0;
1181 } else {
1182#line 875
1183 int tmp_ndt_9;
1184 tmp_ndt_9 = __VERIFIER_nondet_int();
1185 if (tmp_ndt_9 == 1) {
1186 goto switch_4_1;
1187 } else {
1188 goto switch_4_default;
1189#line 880
1190 if (0) {
1191 switch_4_0:
1192#line 882
1193 returnVal2 = 0;
1194 goto switch_4_break;
1195 switch_4_1:
1196#line 885
1197 returnVal2 = -1073741823;
1198 goto switch_4_break;
1199 switch_4_default:
1200#line 888
1201 returnVal2 = 259;
1202 goto switch_4_break;
1203 } else {
1204 switch_4_break: ;
1205 }
1206 }
1207 }
1208#line 896
1209 if (s == NP) {
1210#line 897
1211 s = IPC;
1212#line 898
1213 lowerDriverReturn = returnVal2;
1214 } else {
1215#line 900
1216 if (s == MPR1) {
1217#line 901
1218 if (returnVal2 == 259) {
1219#line 902
1220 s = MPR3;
1221#line 903
1222 lowerDriverReturn = returnVal2;
1223 } else {
1224#line 905
1225 s = NP;
1226#line 906
1227 lowerDriverReturn = returnVal2;
1228 }
1229 } else {
1230#line 909
1231 if (s == SKIP1) {
1232#line 910
1233 s = SKIP2;
1234#line 911
1235 lowerDriverReturn = returnVal2;
1236 } else {
1237 {
1238#line 914
1239 errorFn();
1240 }
1241 }
1242 }
1243 }
1244#line 919
1245 return (returnVal2);
1246}
1247}
1248#line 922 "diskperf_simpl1.cil.c"
1249void IofCompleteRequest(int Irp , int PriorityBoost )
1250{
1251
1252 {
1253#line 926
1254 if (s == NP) {
1255#line 927
1256 s = DC;
1257 } else {
1258 {
1259#line 930
1260 errorFn();
1261 }
1262 }
1263#line 933
1264 return;
1265}
1266}
1267#line 936 "diskperf_simpl1.cil.c"
1268int KeSetEvent(int Event , int Increment , int Wait )
1269{ int l ;
1270
1271 {
1272#line 940
1273 setEventCalled = 1;
1274#line 941
1275 return (l);
1276}
1277}
1278#line 944 "diskperf_simpl1.cil.c"
1279int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
1280 int Timeout )
1281{
1282
1283 {
1284#line 949
1285 if (s == MPR3) {
1286#line 950
1287 if (setEventCalled == 1) {
1288#line 951
1289 s = NP;
1290#line 952
1291 setEventCalled = 0;
1292 } else {
1293 goto _L;
1294 }
1295 } else {
1296 _L:
1297#line 958
1298 if (customIrp == 1) {
1299#line 959
1300 s = NP;
1301#line 960
1302 customIrp = 0;
1303 } else {
1304#line 962
1305 if (s == MPR3) {
1306 {
1307#line 964
1308 errorFn();
1309 }
1310 }
1311 }
1312 }
1313#line 971
1314 int tmp_ndt_10;
1315 tmp_ndt_10 = __VERIFIER_nondet_int();
1316 if (tmp_ndt_10 == 0) {
1317 goto switch_5_0;
1318 } else {
1319 goto switch_5_default;
1320#line 976
1321 if (0) {
1322 switch_5_0: ;
1323#line 978
1324 return (0);
1325 switch_5_default: ;
1326#line 980
1327 return (-1073741823);
1328 } else {
1329
1330 }
1331 }
1332}
1333}
1334#line 988 "diskperf_simpl1.cil.c"
1335int PoCallDriver(int DeviceObject , int Irp )
1336{
1337 int compRetStatus ;
1338 int returnVal ;
1339 int lcontext ;
1340 unsigned long __cil_tmp7 ;
1341 long __cil_tmp8 ;
1342
1343 {
1344#line 995
1345 if (compRegistered) {
1346#line 996
1347 if (routine == 0) {
1348 {
1349#line 998
1350 compRetStatus = DiskPerfIrpCompletion(DeviceObject, Irp, lcontext);
1351 }
1352 } else {
1353#line 1001
1354 if (routine == 1) {
1355 {
1356#line 1003
1357 compRetStatus = DiskPerfIoCompletion(DeviceObject, Irp, lcontext);
1358 }
1359 }
1360 }
1361 {
1362#line 1009
1363 __cil_tmp7 = (unsigned long )compRetStatus;
1364#line 1009
1365 if (__cil_tmp7 == -1073741802) {
1366 {
1367#line 1011
1368 stubMoreProcessingRequired();
1369 }
1370 }
1371 }
1372 }
1373#line 1019
1374 int tmp_ndt_11;
1375 tmp_ndt_11 = __VERIFIER_nondet_int();
1376 if (tmp_ndt_11 == 0) {
1377 goto switch_6_0;
1378 } else {
1379#line 1022
1380 int tmp_ndt_12;
1381 tmp_ndt_12 = __VERIFIER_nondet_int();
1382 if (tmp_ndt_12 == 1) {
1383 goto switch_6_1;
1384 } else {
1385 goto switch_6_default;
1386#line 1027
1387 if (0) {
1388 switch_6_0:
1389#line 1029
1390 returnVal = 0;
1391 goto switch_6_break;
1392 switch_6_1:
1393#line 1032
1394 returnVal = -1073741823;
1395 goto switch_6_break;
1396 switch_6_default:
1397#line 1035
1398 returnVal = 259;
1399 goto switch_6_break;
1400 } else {
1401 switch_6_break: ;
1402 }
1403 }
1404 }
1405#line 1043
1406 if (s == NP) {
1407#line 1044
1408 s = IPC;
1409#line 1045
1410 lowerDriverReturn = returnVal;
1411 } else {
1412#line 1047
1413 if (s == MPR1) {
1414 {
1415#line 1048
1416 __cil_tmp8 = (long )returnVal;
1417#line 1048
1418 if (__cil_tmp8 == 259L) {
1419#line 1049
1420 s = MPR3;
1421#line 1050
1422 lowerDriverReturn = returnVal;
1423 } else {
1424#line 1052
1425 s = NP;
1426#line 1053
1427 lowerDriverReturn = returnVal;
1428 }
1429 }
1430 } else {
1431#line 1056
1432 if (s == SKIP1) {
1433#line 1057
1434 s = SKIP2;
1435#line 1058
1436 lowerDriverReturn = returnVal;
1437 } else {
1438 {
1439#line 1061
1440 errorFn();
1441 }
1442 }
1443 }
1444 }
1445#line 1066
1446 return (returnVal);
1447}
1448}