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