source: CIVL/examples/svcomp17/floppy_simpl4_false-unreach-call_true-termination.cil.c@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 45.3 KB
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2
3extern char __VERIFIER_nondet_char(void);
4extern int __VERIFIER_nondet_int(void);
5extern long __VERIFIER_nondet_long(void);
6extern void *__VERIFIER_nondet_pointer(void);
7void errorFn(void) ;
8void IofCompleteRequest(int Irp , int PriorityBoost );
9extern int __VERIFIER_nondet_int();
10int FloppyThread ;
11int KernelMode ;
12int Suspended ;
13int Executive ;
14int DiskController ;
15int FloppyDiskPeripheral ;
16int FlConfigCallBack ;
17int MaximumInterfaceType ;
18int MOUNTDEV_MOUNTED_DEVICE_GUID ;
19int myStatus ;
20int s ;
21int UNLOADED ;
22int NP ;
23int DC ;
24int SKIP1 ;
25int SKIP2 ;
26int MPR1 ;
27int MPR3 ;
28int IPC ;
29int pended ;
30int compRegistered ;
31int lowerDriverReturn ;
32int setEventCalled ;
33int customIrp ;
34
35void _BLAST_init(void)
36{
37
38 {
39 UNLOADED = 0;
40 NP = 1;
41 DC = 2;
42 SKIP1 = 3;
43 SKIP2 = 4;
44 MPR1 = 5;
45 MPR3 = 6;
46 IPC = 7;
47 s = UNLOADED;
48 pended = 0;
49 compRegistered = 0;
50 lowerDriverReturn = 0;
51 setEventCalled = 0;
52 customIrp = 0;
53 return;
54}
55}
56int PagingReferenceCount = 0;
57int PagingMutex = 0;
58int FlAcpiConfigureFloppy(int DisketteExtension , int FdcInfo )
59{
60
61 {
62 return (0);
63}
64}
65int FlQueueIrpToThread(int Irp , int DisketteExtension )
66{ int status ;
67 int threadHandle = __VERIFIER_nondet_int() ;
68 int DisketteExtension__PoweringDown = __VERIFIER_nondet_int() ;
69 int DisketteExtension__ThreadReferenceCount = __VERIFIER_nondet_int() ;
70 int DisketteExtension__FloppyThread = __VERIFIER_nondet_int() ;
71 int Irp__IoStatus__Status ;
72 int Irp__IoStatus__Information ;
73 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
74 int ObjAttributes = __VERIFIER_nondet_int() ;
75 int __cil_tmp12 ;
76 int __cil_tmp13 ;
77
78 {
79 if (DisketteExtension__PoweringDown == 1) {
80 myStatus = -1073741101;
81 Irp__IoStatus__Status = -1073741101;
82 Irp__IoStatus__Information = 0;
83 return (-1073741101);
84 }
85 DisketteExtension__ThreadReferenceCount ++;
86 if (DisketteExtension__ThreadReferenceCount == 0) {
87 DisketteExtension__ThreadReferenceCount ++;
88 PagingReferenceCount ++;
89 if (PagingReferenceCount == 1) {
90
91 }
92 {
93 status = PsCreateSystemThread(threadHandle, 0, ObjAttributes, 0, 0, FloppyThread,
94 DisketteExtension);
95 }
96 {
97 if (status < 0) {
98 DisketteExtension__ThreadReferenceCount = -1;
99 PagingReferenceCount --;
100 if (PagingReferenceCount == 0) {
101
102 }
103 return (status);
104 }
105 }
106 {
107 status = ObReferenceObjectByHandle(threadHandle, 1048576, 0, KernelMode, DisketteExtension__FloppyThread,
108 0);
109 ZwClose(threadHandle);
110 }
111 {
112 if (status < 0) {
113 return (status);
114 }
115 }
116 }
117 //Irp__Tail__Overlay__CurrentStackLocation__Control |= 1;
118 if (pended == 0) {
119 pended = 1;
120 } else {
121 {
122 errorFn();
123 }
124 }
125 return (259);
126}
127}
128int FloppyPnp(int DeviceObject , int Irp )
129{ int DeviceObject__DeviceExtension = __VERIFIER_nondet_int() ;
130 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
131 int Irp__IoStatus__Information ;
132 int Irp__IoStatus__Status ;
133 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
134 int disketteExtension__IsRemoved = __VERIFIER_nondet_int() ;
135 int disketteExtension__IsStarted = __VERIFIER_nondet_int() ;
136 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
137 int disketteExtension__HoldNewRequests ;
138 int disketteExtension__FloppyThread = __VERIFIER_nondet_int() ;
139 int disketteExtension__InterfaceString__Buffer = __VERIFIER_nondet_int() ;
140 int disketteExtension__InterfaceString = __VERIFIER_nondet_int() ;
141 int disketteExtension__ArcName__Length = __VERIFIER_nondet_int() ;
142 int disketteExtension__ArcName = __VERIFIER_nondet_int() ;
143 int irpSp__MinorFunction = __VERIFIER_nondet_int() ;
144 int IoGetConfigurationInformation__FloppyCount = __VERIFIER_nondet_int() ;
145 int irpSp ;
146 int disketteExtension ;
147 int ntStatus ;
148 int doneEvent = __VERIFIER_nondet_int() ;
149 int irpSp___0 ;
150 int nextIrpSp ;
151 int nextIrpSp__Control ;
152 int irpSp___1 ;
153 int irpSp__Context ;
154 int irpSp__Control ;
155 long __cil_tmp29 ;
156 long __cil_tmp30 ;
157
158 {
159 ntStatus = 0;
160 PagingReferenceCount ++;
161 if (PagingReferenceCount == 1) {
162
163 }
164 disketteExtension = DeviceObject__DeviceExtension;
165 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
166 if (disketteExtension__IsRemoved) {
167 {
168 Irp__IoStatus__Information = 0;
169 Irp__IoStatus__Status = -1073741738;
170 myStatus = -1073741738;
171 IofCompleteRequest(Irp, 0);
172 }
173 return (-1073741738);
174 }
175 if (irpSp__MinorFunction == 0) {
176 goto switch_0_0;
177 } else {
178 if (irpSp__MinorFunction == 5) {
179 goto switch_0_5;
180 } else {
181 if (irpSp__MinorFunction == 1) {
182 goto switch_0_5;
183 } else {
184 if (irpSp__MinorFunction == 6) {
185 goto switch_0_6;
186 } else {
187 if (irpSp__MinorFunction == 3) {
188 goto switch_0_6;
189 } else {
190 if (irpSp__MinorFunction == 4) {
191 goto switch_0_4;
192 } else {
193 if (irpSp__MinorFunction == 2) {
194 goto switch_0_2;
195 } else {
196 goto switch_0_default;
197 if (0) {
198 switch_0_0:
199 {
200 ntStatus = FloppyStartDevice(DeviceObject, Irp);
201 }
202 goto switch_0_break;
203 switch_0_5:
204 if (irpSp__MinorFunction == 5) {
205
206 }
207 if (! disketteExtension__IsStarted) {
208 if (s == NP) {
209 s = SKIP1;
210 } else {
211 {
212 errorFn();
213 }
214 }
215 {
216 Irp__CurrentLocation ++;
217 Irp__Tail__Overlay__CurrentStackLocation ++;
218 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
219 }
220 return (ntStatus);
221 }
222 {
223 disketteExtension__HoldNewRequests = 1;
224 ntStatus = FlQueueIrpToThread(Irp, disketteExtension);
225 }
226 {
227 __cil_tmp29 = (long )ntStatus;
228 if (__cil_tmp29 == 259L) {
229 {
230 KeWaitForSingleObject(disketteExtension__FloppyThread, Executive,
231 KernelMode, 0, 0);
232 }
233 if (disketteExtension__FloppyThread != 0) {
234
235 }
236 disketteExtension__FloppyThread = 0;
237 Irp__IoStatus__Status = 0;
238 myStatus = 0;
239 if (s == NP) {
240 s = SKIP1;
241 } else {
242 {
243 errorFn();
244 }
245 }
246 {
247 Irp__CurrentLocation ++;
248 Irp__Tail__Overlay__CurrentStackLocation ++;
249 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
250 }
251 } else {
252 {
253 ntStatus = -1073741823;
254 Irp__IoStatus__Status = ntStatus;
255 myStatus = ntStatus;
256 Irp__IoStatus__Information = 0;
257 IofCompleteRequest(Irp, 0);
258 }
259 }
260 }
261 goto switch_0_break;
262 switch_0_6:
263 if (irpSp__MinorFunction == 6) {
264
265 }
266 if (! disketteExtension__IsStarted) {
267 Irp__IoStatus__Status = 0;
268 myStatus = 0;
269 if (s == NP) {
270 s = SKIP1;
271 } else {
272 {
273 errorFn();
274 }
275 }
276 {
277 Irp__CurrentLocation ++;
278 Irp__Tail__Overlay__CurrentStackLocation ++;
279 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
280 }
281 } else {
282 Irp__IoStatus__Status = 0;
283 myStatus = 0;
284 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
285 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
286 nextIrpSp__Control = 0;
287 if (s != NP) {
288 {
289 errorFn();
290 }
291 } else {
292 if (compRegistered != 0) {
293 {
294 errorFn();
295 }
296 } else {
297 compRegistered = 1;
298 }
299 }
300 {
301 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
302 irpSp__Context = doneEvent;
303 irpSp__Control = 224;
304 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
305 }
306 {
307 __cil_tmp30 = (long )ntStatus;
308 if (__cil_tmp30 == 259L) {
309 {
310 KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
311 ntStatus = myStatus;
312 }
313 }
314 }
315 {
316 disketteExtension__HoldNewRequests = 0;
317 Irp__IoStatus__Status = ntStatus;
318 myStatus = ntStatus;
319 Irp__IoStatus__Information = 0;
320 IofCompleteRequest(Irp, 0);
321 }
322 }
323 goto switch_0_break;
324 switch_0_4:
325 disketteExtension__IsStarted = 0;
326 Irp__IoStatus__Status = 0;
327 myStatus = 0;
328 if (s == NP) {
329 s = SKIP1;
330 } else {
331 {
332 errorFn();
333 }
334 }
335 {
336 Irp__CurrentLocation ++;
337 Irp__Tail__Overlay__CurrentStackLocation ++;
338 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
339 }
340 goto switch_0_break;
341 switch_0_2:
342 disketteExtension__HoldNewRequests = 0;
343 disketteExtension__IsStarted = 0;
344 disketteExtension__IsRemoved = 1;
345 if (s == NP) {
346 s = SKIP1;
347 } else {
348 {
349 errorFn();
350 }
351 }
352 {
353 Irp__CurrentLocation ++;
354 Irp__Tail__Overlay__CurrentStackLocation ++;
355 Irp__IoStatus__Status = 0;
356 myStatus = 0;
357 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
358 }
359 if (disketteExtension__InterfaceString__Buffer != 0) {
360 {
361 IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
362 0);
363 }
364 }
365 if (disketteExtension__ArcName__Length != 0) {
366 {
367 IoDeleteSymbolicLink(disketteExtension__ArcName);
368 }
369 }
370 IoGetConfigurationInformation__FloppyCount --;
371 goto switch_0_break;
372 switch_0_default: ;
373 if (s == NP) {
374 s = SKIP1;
375 } else {
376 {
377 errorFn();
378 }
379 }
380 {
381 Irp__CurrentLocation ++;
382 Irp__Tail__Overlay__CurrentStackLocation ++;
383 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
384 }
385 } else {
386 switch_0_break: ;
387 }
388 }
389 }
390 }
391 }
392 }
393 }
394 }
395 PagingReferenceCount --;
396 if (PagingReferenceCount == 0) {
397
398 }
399 return (ntStatus);
400}
401}
402int FloppyStartDevice(int DeviceObject , int Irp )
403{ int DeviceObject__DeviceExtension = __VERIFIER_nondet_int() ;
404 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
405 int Irp__IoStatus__Status ;
406 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
407 int disketteExtension__MaxTransferSize ;
408 int disketteExtension__DriveType = __VERIFIER_nondet_int() ;
409 int disketteExtension__PerpendicularMode ;
410 int disketteExtension__DeviceUnit ;
411 int disketteExtension__DriveOnValue ;
412 int disketteExtension__UnderlyingPDO = __VERIFIER_nondet_int() ;
413 int disketteExtension__InterfaceString = __VERIFIER_nondet_int() ;
414 int disketteExtension__IsStarted ;
415 int disketteExtension__HoldNewRequests ;
416 int ntStatus ;
417 int pnpStatus ;
418 int doneEvent = __VERIFIER_nondet_int() ;
419 int fdcInfo = __VERIFIER_nondet_int() ;
420 int fdcInfo__BufferCount ;
421 int fdcInfo__BufferSize ;
422 int fdcInfo__MaxTransferSize = __VERIFIER_nondet_int() ;
423 int fdcInfo__AcpiBios = __VERIFIER_nondet_int() ;
424 int fdcInfo__AcpiFdiSupported = __VERIFIER_nondet_int() ;
425 int fdcInfo__PeripheralNumber = __VERIFIER_nondet_int() ;
426 int fdcInfo__BusType ;
427 int fdcInfo__ControllerNumber = __VERIFIER_nondet_int() ;
428 int fdcInfo__UnitNumber = __VERIFIER_nondet_int() ;
429 int fdcInfo__BusNumber = __VERIFIER_nondet_int() ;
430 int Dc ;
431 int Fp ;
432 int disketteExtension ;
433 int irpSp ;
434 int irpSp___0 ;
435 int nextIrpSp ;
436 int nextIrpSp__Control ;
437 int irpSp___1 ;
438 int irpSp__Control ;
439 int irpSp__Context ;
440 int InterfaceType ;
441 int KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 = __VERIFIER_nondet_int() ;
442 long __cil_tmp42 ;
443 int __cil_tmp43 ;
444 int __cil_tmp44 ;
445 int __cil_tmp45 ;
446 int __cil_tmp46 = __VERIFIER_nondet_int() ;
447 int __cil_tmp47 ;
448 int __cil_tmp48 ;
449 int __cil_tmp49 ;
450
451 {
452 Dc = DiskController;
453 Fp = FloppyDiskPeripheral;
454 disketteExtension = DeviceObject__DeviceExtension;
455 irpSp = Irp__Tail__Overlay__CurrentStackLocation;
456 irpSp___0 = Irp__Tail__Overlay__CurrentStackLocation;
457 nextIrpSp = Irp__Tail__Overlay__CurrentStackLocation - 1;
458 nextIrpSp__Control = 0;
459 if (s != NP) {
460 {
461 errorFn();
462 }
463 } else {
464 if (compRegistered != 0) {
465 {
466 errorFn();
467 }
468 } else {
469 compRegistered = 1;
470 }
471 }
472 {
473 irpSp___1 = Irp__Tail__Overlay__CurrentStackLocation - 1;
474 irpSp__Context = doneEvent;
475 irpSp__Control = 224;
476 ntStatus = IofCallDriver(disketteExtension__TargetObject, Irp);
477 }
478 {
479 __cil_tmp42 = (long )ntStatus;
480 if (__cil_tmp42 == 259L) {
481 {
482 ntStatus = KeWaitForSingleObject(doneEvent, Executive, KernelMode, 0, 0);
483 ntStatus = myStatus;
484 }
485 }
486 }
487 {
488 fdcInfo__BufferCount = 0;
489 fdcInfo__BufferSize = 0;
490 //__cil_tmp43 = 770 << 2;
491 //__cil_tmp44 = 7 << 16;
492 //__cil_tmp45 = __cil_tmp44 | __cil_tmp43;
493 //__cil_tmp46 = __cil_tmp45 | 3;
494 ntStatus = FlFdcDeviceIo(disketteExtension__TargetObject, __cil_tmp46, fdcInfo);
495 }
496 if (ntStatus >= 0) {
497 disketteExtension__MaxTransferSize = fdcInfo__MaxTransferSize;
498 if (fdcInfo__AcpiBios) {
499 if (fdcInfo__AcpiFdiSupported) {
500 {
501 ntStatus = FlAcpiConfigureFloppy(disketteExtension, fdcInfo);
502 }
503 if (disketteExtension__DriveType == 4) {
504 // __cil_tmp47 = 1 << fdcInfo__PeripheralNumber;
505 //disketteExtension__PerpendicularMode |= __cil_tmp47;
506 }
507 } else {
508 goto _L;
509 }
510 } else {
511 _L:
512 if (disketteExtension__DriveType == 4) {
513 // __cil_tmp48 = 1 << fdcInfo__PeripheralNumber;
514 //disketteExtension__PerpendicularMode |= __cil_tmp48;
515 }
516 InterfaceType = 0;
517 {
518 while (1) {
519 while_0_continue: /* CIL Label */ ;
520
521 if (InterfaceType >= MaximumInterfaceType) {
522 goto while_1_break;
523 }
524 {
525 fdcInfo__BusType = InterfaceType;
526 ntStatus = IoQueryDeviceDescription(fdcInfo__BusType, fdcInfo__BusNumber,
527 Dc, fdcInfo__ControllerNumber, Fp, fdcInfo__PeripheralNumber,
528 FlConfigCallBack, disketteExtension);
529 }
530 if (ntStatus >= 0) {
531 goto while_1_break;
532 }
533 InterfaceType ++;
534 }
535 while_0_break: /* CIL Label */ ;
536 }
537 while_1_break: ;
538 }
539 if (ntStatus >= 0) {
540 if (KUSER_SHARED_DATA__AlternativeArchitecture_NEC98x86 != 0) {
541 disketteExtension__DeviceUnit = fdcInfo__UnitNumber;
542 disketteExtension__DriveOnValue = fdcInfo__UnitNumber;
543 } else {
544 disketteExtension__DeviceUnit = fdcInfo__PeripheralNumber;
545 //__cil_tmp49 = 16 << fdcInfo__PeripheralNumber;
546 //disketteExtension__DriveOnValue = fdcInfo__PeripheralNumber | __cil_tmp49;
547 }
548 {
549 pnpStatus = IoRegisterDeviceInterface(disketteExtension__UnderlyingPDO, MOUNTDEV_MOUNTED_DEVICE_GUID,
550 0, disketteExtension__InterfaceString);
551 }
552 if (pnpStatus >= 0) {
553 {
554 pnpStatus = IoSetDeviceInterfaceState(disketteExtension__InterfaceString,
555 1);
556 }
557 }
558 disketteExtension__IsStarted = 1;
559 disketteExtension__HoldNewRequests = 0;
560 }
561 }
562 {
563 Irp__IoStatus__Status = ntStatus;
564 myStatus = ntStatus;
565 IofCompleteRequest(Irp, 0);
566 }
567 return (ntStatus);
568}
569}
570int FloppyPnpComplete(int DeviceObject , int Irp , int Context )
571{
572
573 {
574 {
575 KeSetEvent(Context, 1, 0);
576 }
577 return (-1073741802);
578}
579}
580int FlFdcDeviceIo(int DeviceObject , int Ioctl , int Data )
581{ int ntStatus ;
582 int irp ;
583 int irpStack ;
584 int doneEvent = __VERIFIER_nondet_int() ;
585 int ioStatus = __VERIFIER_nondet_int() ;
586 int irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
587 int irpStack__Parameters__DeviceIoControl__Type3InputBuffer ;
588 long __cil_tmp11 ;
589
590 {
591 {
592 irp = IoBuildDeviceIoControlRequest(Ioctl, DeviceObject, 0, 0, 0, 0, 1, doneEvent,
593 ioStatus);
594 }
595 if (irp == 0) {
596 return (-1073741670);
597 }
598 {
599 irpStack = irp__Tail__Overlay__CurrentStackLocation - 1;
600 irpStack__Parameters__DeviceIoControl__Type3InputBuffer = Data;
601 ntStatus = IofCallDriver(DeviceObject, irp);
602 }
603 {
604 __cil_tmp11 = (long )ntStatus;
605 if (__cil_tmp11 == 259L) {
606 {
607 KeWaitForSingleObject(doneEvent, Suspended, KernelMode, 0, 0);
608 ntStatus = myStatus;
609 }
610 }
611 }
612 return (ntStatus);
613}
614}
615void FloppyProcessQueuedRequests(int DisketteExtension )
616{
617
618 {
619 return;
620}
621}
622void stub_driver_init(void)
623{
624
625 {
626 s = NP;
627 pended = 0;
628 compRegistered = 0;
629 lowerDriverReturn = 0;
630 setEventCalled = 0;
631 customIrp = 0;
632 return;
633}
634}
635int main(void)
636{ int status ;
637 int irp = __VERIFIER_nondet_int() ;
638 int pirp ;
639 int pirp__IoStatus__Status ;
640 int irp_choice = __VERIFIER_nondet_int() ;
641 int devobj = __VERIFIER_nondet_int() ;
642 int __cil_tmp8 ;
643
644 FloppyThread = 0;
645 KernelMode = 0;
646 Suspended = 0;
647 Executive = 0;
648 DiskController = 0;
649 FloppyDiskPeripheral = 0;
650 FlConfigCallBack = 0;
651 MaximumInterfaceType = 0;
652 MOUNTDEV_MOUNTED_DEVICE_GUID = 0;
653 myStatus = 0;
654 s = 0;
655 UNLOADED = 0;
656 NP = 0;
657 DC = 0;
658 SKIP1 = 0;
659 SKIP2 = 0 ;
660 MPR1 = 0;
661 MPR3 = 0;
662 IPC = 0;
663 pended = 0;
664 compRegistered = 0;
665 lowerDriverReturn = 0;
666 setEventCalled = 0;
667 customIrp = 0;
668
669 {
670 {
671 status = 0;
672 pirp = irp;
673 _BLAST_init();
674 }
675 if (status >= 0) {
676 s = NP;
677 customIrp = 0;
678 setEventCalled = customIrp;
679 lowerDriverReturn = setEventCalled;
680 compRegistered = lowerDriverReturn;
681 pended = compRegistered;
682 pirp__IoStatus__Status = 0;
683 myStatus = 0;
684 if (irp_choice == 0) {
685 pirp__IoStatus__Status = -1073741637;
686 myStatus = -1073741637;
687 }
688 {
689 stub_driver_init();
690 }
691 {
692 if (status < 0) {
693 return (-1);
694 }
695 }
696 int tmp_ndt_1;
697 tmp_ndt_1 = __VERIFIER_nondet_int();
698 if (tmp_ndt_1 == 0) {
699 goto switch_2_0;
700 } else {
701 int tmp_ndt_2;
702 tmp_ndt_2 = __VERIFIER_nondet_int();
703 if (tmp_ndt_2 == 1) {
704 goto switch_2_1;
705 } else {
706 int tmp_ndt_3;
707 tmp_ndt_3 = __VERIFIER_nondet_int();
708 if (tmp_ndt_3 == 2) {
709 goto switch_2_2;
710 } else {
711 int tmp_ndt_4;
712 tmp_ndt_4 = __VERIFIER_nondet_int();
713 if (tmp_ndt_4 == 3) {
714 goto switch_2_3;
715 } else {
716 goto switch_2_default;
717 if (0) {
718 switch_2_0:
719 {
720 status = FloppyCreateClose(devobj, pirp);
721 }
722 goto switch_2_break;
723 switch_2_1:
724 {
725 status = FloppyCreateClose(devobj, pirp);
726 }
727 goto switch_2_break;
728 switch_2_2:
729 {
730 status = FloppyDeviceControl(devobj, pirp);
731 }
732 goto switch_2_break;
733 switch_2_3:
734 {
735 status = FloppyPnp(devobj, pirp);
736 }
737 goto switch_2_break;
738 switch_2_default: ;
739 return (-1);
740 } else {
741 switch_2_break: ;
742 }
743 }
744 }
745 }
746 }
747 }
748 if (pended == 1) {
749 if (s == NP) {
750 s = NP;
751 } else {
752 goto _L___2;
753 }
754 } else {
755 _L___2:
756 if (pended == 1) {
757 if (s == MPR3) {
758 s = MPR3;
759 } else {
760 goto _L___1;
761 }
762 } else {
763 _L___1:
764 if (s != UNLOADED) {
765 if (status != -1) {
766 if (s != SKIP2) {
767 if (s != IPC) {
768 if (s != DC) {
769 {
770 errorFn();
771 }
772 } else {
773 goto _L___0;
774 }
775 } else {
776 goto _L___0;
777 }
778 } else {
779 _L___0:
780 if (pended == 1) {
781 if (status != 259) {
782 errorFn();
783 }
784 } else {
785 if (s == DC) {
786 if (status == 259) {
787 {
788 errorFn();
789 }
790 }
791 } else {
792 if (status != lowerDriverReturn) {
793 {
794 errorFn();
795 }
796 }
797 }
798 }
799 }
800 }
801 }
802 }
803 }
804 status = 0;
805 return (status);
806}
807}
808int IoBuildDeviceIoControlRequest(int IoControlCode , int DeviceObject , int InputBuffer ,
809 int InputBufferLength , int OutputBuffer , int OutputBufferLength ,
810 int InternalDeviceIoControl , int Event , int IoStatusBlock )
811{
812 int malloc = __VERIFIER_nondet_int() ;
813
814 {
815 customIrp = 1;
816 int tmp_ndt_5;
817 tmp_ndt_5 = __VERIFIER_nondet_int();
818 if (tmp_ndt_5 == 0) {
819 goto switch_3_0;
820 } else {
821 goto switch_3_default;
822 if (0) {
823 switch_3_0:
824 return (malloc);
825 switch_3_default: ;
826 return (0);
827 } else {
828
829 }
830 }
831}
832}
833int IoDeleteSymbolicLink(int SymbolicLinkName )
834{
835
836 {
837 int tmp_ndt_6;
838 tmp_ndt_6 = __VERIFIER_nondet_int();
839 if (tmp_ndt_6 == 0) {
840 goto switch_4_0;
841 } else {
842 goto switch_4_default;
843 if (0) {
844 switch_4_0:
845 return (0);
846 switch_4_default: ;
847 return (-1073741823);
848 } else {
849
850 }
851 }
852}
853}
854int IoQueryDeviceDescription(int BusType , int BusNumber , int ControllerType , int ControllerNumber ,
855 int PeripheralType , int PeripheralNumber , int CalloutRoutine ,
856 int Context )
857{
858
859 {
860 int tmp_ndt_7;
861 tmp_ndt_7 = __VERIFIER_nondet_int();
862 if (tmp_ndt_7 == 0) {
863 goto switch_5_0;
864 } else {
865 goto switch_5_default;
866 if (0) {
867 switch_5_0:
868 return (0);
869 switch_5_default: ;
870 return (-1073741823);
871 } else {
872
873 }
874 }
875}
876}
877int IoRegisterDeviceInterface(int PhysicalDeviceObject , int InterfaceClassGuid ,
878 int ReferenceString , int SymbolicLinkName )
879{
880
881 {
882 int tmp_ndt_8;
883 tmp_ndt_8 = __VERIFIER_nondet_int();
884 if (tmp_ndt_8 == 0) {
885 goto switch_6_0;
886 } else {
887 goto switch_6_default;
888 if (0) {
889 switch_6_0:
890 return (0);
891 switch_6_default: ;
892 return (-1073741808);
893 } else {
894
895 }
896 }
897}
898}
899int IoSetDeviceInterfaceState(int SymbolicLinkName , int Enable )
900{
901
902 {
903 int tmp_ndt_9;
904 tmp_ndt_9 = __VERIFIER_nondet_int();
905 if (tmp_ndt_9 == 0) {
906 goto switch_7_0;
907 } else {
908 goto switch_7_default;
909 if (0) {
910 switch_7_0:
911 return (0);
912 switch_7_default: ;
913 return (-1073741823);
914 } else {
915
916 }
917 }
918}
919}
920void stubMoreProcessingRequired(void)
921{
922
923 {
924 if (s == NP) {
925 s = MPR1;
926 } else {
927 {
928 errorFn();
929 }
930 }
931 return;
932}
933}
934int IofCallDriver(int DeviceObject , int Irp )
935{
936 int returnVal2 ;
937 int compRetStatus1 ;
938 int lcontext = __VERIFIER_nondet_int() ;
939 unsigned long __cil_tmp7 ;
940
941 {
942 if (compRegistered) {
943 {
944 compRetStatus1 = FloppyPnpComplete(DeviceObject, Irp, lcontext);
945 }
946 {
947 __cil_tmp7 = (unsigned long )compRetStatus1;
948 if (__cil_tmp7 == -1073741802) {
949 {
950 stubMoreProcessingRequired();
951 }
952 }
953 }
954 }
955 int tmp_ndt_10;
956 tmp_ndt_10 = __VERIFIER_nondet_int();
957 if (tmp_ndt_10 == 0) {
958 goto switch_8_0;
959 } else {
960 int tmp_ndt_11;
961 tmp_ndt_11 = __VERIFIER_nondet_int();
962 if (tmp_ndt_11 == 1) {
963 goto switch_8_1;
964 } else {
965 goto switch_8_default;
966 if (0) {
967 switch_8_0:
968 returnVal2 = 0;
969 goto switch_8_break;
970 switch_8_1:
971 returnVal2 = -1073741823;
972 goto switch_8_break;
973 switch_8_default:
974 returnVal2 = 259;
975 goto switch_8_break;
976 } else {
977 switch_8_break: ;
978 }
979 }
980 }
981 if (s == NP) {
982 s = IPC;
983 lowerDriverReturn = returnVal2;
984 } else {
985 if (s == MPR1) {
986 if (returnVal2 == 259) {
987 s = MPR3;
988 lowerDriverReturn = returnVal2;
989 } else {
990 s = NP;
991 lowerDriverReturn = returnVal2;
992 }
993 } else {
994 if (s == SKIP1) {
995 s = SKIP2;
996 lowerDriverReturn = returnVal2;
997 } else {
998 {
999 errorFn();
1000 }
1001 }
1002 }
1003 }
1004 return (returnVal2);
1005}
1006}
1007void IofCompleteRequest(int Irp , int PriorityBoost )
1008{
1009
1010 {
1011 if (s == NP) {
1012 s = DC;
1013 } else {
1014 {
1015 errorFn();
1016 }
1017 }
1018 return;
1019}
1020}
1021int KeSetEvent(int Event , int Increment , int Wait )
1022{ int l = __VERIFIER_nondet_int() ;
1023
1024 {
1025 setEventCalled = 1;
1026 return (l);
1027}
1028}
1029int KeWaitForSingleObject(int Object , int WaitReason , int WaitMode , int Alertable ,
1030 int Timeout )
1031{
1032
1033 {
1034 if (s == MPR3) {
1035 if (setEventCalled == 1) {
1036 s = NP;
1037 setEventCalled = 0;
1038 } else {
1039 goto _L;
1040 }
1041 } else {
1042 _L:
1043 if (customIrp == 1) {
1044 s = NP;
1045 customIrp = 0;
1046 } else {
1047 if (s == MPR3) {
1048 {
1049 errorFn();
1050 }
1051 }
1052 }
1053 }
1054 int tmp_ndt_12;
1055 tmp_ndt_12 = __VERIFIER_nondet_int();
1056 if (tmp_ndt_12 == 0) {
1057 goto switch_9_0;
1058 } else {
1059 goto switch_9_default;
1060 if (0) {
1061 switch_9_0:
1062 return (0);
1063 switch_9_default: ;
1064 return (-1073741823);
1065 } else {
1066
1067 }
1068 }
1069}
1070}
1071int ObReferenceObjectByHandle(int Handle , int DesiredAccess , int ObjectType , int AccessMode ,
1072 int Object , int HandleInformation )
1073{
1074
1075 {
1076 int tmp_ndt_13;
1077 tmp_ndt_13 = __VERIFIER_nondet_int();
1078 if (tmp_ndt_13 == 0) {
1079 goto switch_10_0;
1080 } else {
1081 goto switch_10_default;
1082 if (0) {
1083 switch_10_0:
1084 return (0);
1085 switch_10_default: ;
1086 return (-1073741823);
1087 } else {
1088
1089 }
1090 }
1091}
1092}
1093int PsCreateSystemThread(int ThreadHandle , int DesiredAccess , int ObjectAttributes ,
1094 int ProcessHandle , int ClientId , int StartRoutine , int StartContext )
1095{
1096
1097 {
1098 int tmp_ndt_14;
1099 tmp_ndt_14 = __VERIFIER_nondet_int();
1100 if (tmp_ndt_14 == 0) {
1101 goto switch_11_0;
1102 } else {
1103 goto switch_11_default;
1104 if (0) {
1105 switch_11_0:
1106 return (0);
1107 switch_11_default: ;
1108 return (-1073741823);
1109 } else {
1110
1111 }
1112 }
1113}
1114}
1115int ZwClose(int Handle )
1116{
1117
1118 {
1119 int tmp_ndt_15;
1120 tmp_ndt_15 = __VERIFIER_nondet_int();
1121 if (tmp_ndt_15 == 0) {
1122 goto switch_12_0;
1123 } else {
1124 goto switch_12_default;
1125 if (0) {
1126 switch_12_0:
1127 return (0);
1128 switch_12_default: ;
1129 return (-1073741823);
1130 } else {
1131
1132 }
1133 }
1134}
1135}
1136int FloppyCreateClose(int DeviceObject , int Irp )
1137{ int Irp__IoStatus__Status ;
1138 int Irp__IoStatus__Information ;
1139
1140 {
1141 {
1142 myStatus = 0;
1143 Irp__IoStatus__Status = 0;
1144 Irp__IoStatus__Information = 1;
1145 IofCompleteRequest(Irp, 0);
1146 }
1147 return (0);
1148}
1149}
1150int FloppyQueueRequest(int DisketteExtension , int Irp ) ;
1151int FloppyDeviceControl(int DeviceObject , int Irp )
1152{ int disketteExtension__HoldNewRequests = __VERIFIER_nondet_int() ;
1153 int disketteExtension__IsRemoved = __VERIFIER_nondet_int() ;
1154 int Irp__IoStatus__Information ;
1155 int disketteExtension__IsStarted = __VERIFIER_nondet_int() ;
1156 int Irp__CurrentLocation = __VERIFIER_nondet_int() ;
1157 int Irp__Tail__Overlay__CurrentStackLocation = __VERIFIER_nondet_int() ;
1158 int disketteExtension__TargetObject = __VERIFIER_nondet_int() ;
1159 int irpSp__Parameters__DeviceIoControl__OutputBufferLength = __VERIFIER_nondet_int() ;
1160 int sizeof__MOUNTDEV_NAME = __VERIFIER_nondet_int() ;
1161 int Irp__AssociatedIrp__SystemBuffer = __VERIFIER_nondet_int() ;
1162 int mountName__NameLength ;
1163 int disketteExtension__DeviceName__Length = __VERIFIER_nondet_int() ;
1164 int sizeof__USHORT = __VERIFIER_nondet_int() ;
1165 int disketteExtension__InterfaceString__Buffer = __VERIFIER_nondet_int() ;
1166 int uniqueId__UniqueIdLength ;
1167 int disketteExtension__InterfaceString__Length = __VERIFIER_nondet_int() ;
1168 int sizeof__MOUNTDEV_UNIQUE_ID = __VERIFIER_nondet_int() ;
1169 int irpSp__Parameters__DeviceIoControl__InputBufferLength = __VERIFIER_nondet_int() ;
1170 int sizeof__FORMAT_PARAMETERS = __VERIFIER_nondet_int() ;
1171 int irpSp__Parameters__DeviceIoControl__IoControlCode___1 = __VERIFIER_nondet_int() ;
1172 int sizeof__FORMAT_EX_PARAMETERS = __VERIFIER_nondet_int() ;
1173 int formatExParameters__FormatGapLength = __VERIFIER_nondet_int() ;
1174 int formatExParameters__SectorsPerTrack = __VERIFIER_nondet_int() ;
1175 int sizeof__DISK_GEOMETRY = __VERIFIER_nondet_int() ;
1176 int Irp__IoStatus__Status___0 ;
1177 int disketteExtension = __VERIFIER_nondet_int() ;
1178 int ntStatus ;
1179 int outputBufferLength ;
1180 int lowestDriveMediaType = __VERIFIER_nondet_int() ;
1181 int highestDriveMediaType = __VERIFIER_nondet_int() ;
1182 int formatExParametersSize = __VERIFIER_nondet_int() ;
1183 int formatExParameters ;
1184 int tmp ;
1185 int mountName ;
1186 int uniqueId ;
1187 int tmp___0 ;
1188 int __cil_tmp39 ;
1189 int __cil_tmp40 ;
1190 int __cil_tmp41 = __VERIFIER_nondet_int() ;
1191 int __cil_tmp42 ;
1192 int __cil_tmp43 ;
1193 int __cil_tmp44 = __VERIFIER_nondet_int() ;
1194 int __cil_tmp45 = __VERIFIER_nondet_int() ;
1195 int __cil_tmp46 ;
1196 int __cil_tmp47 ;
1197 int __cil_tmp48 ;
1198 int __cil_tmp49 ;
1199 int __cil_tmp50 = __VERIFIER_nondet_int() ;
1200 int __cil_tmp51 ;
1201 int __cil_tmp52 ;
1202 int __cil_tmp53 ;
1203 int __cil_tmp54 ;
1204 int __cil_tmp55 = __VERIFIER_nondet_int() ;
1205 int __cil_tmp56 ;
1206 int __cil_tmp57 ;
1207 int __cil_tmp58 ;
1208 int __cil_tmp59 ;
1209 int __cil_tmp60 = __VERIFIER_nondet_int() ;
1210 int __cil_tmp61 ;
1211 int __cil_tmp62 ;
1212 int __cil_tmp63 ;
1213 int __cil_tmp64 ;
1214 int __cil_tmp65 = __VERIFIER_nondet_int() ;
1215 int __cil_tmp66 = __VERIFIER_nondet_int() ;
1216 int __cil_tmp67 ;
1217 int __cil_tmp68 ;
1218 int __cil_tmp69 = __VERIFIER_nondet_int() ;
1219 int __cil_tmp70 ;
1220 int __cil_tmp71 ;
1221 int __cil_tmp72 = __VERIFIER_nondet_int() ;
1222 int __cil_tmp73 ;
1223 int __cil_tmp74 ;
1224 int __cil_tmp75 = __VERIFIER_nondet_int() ;
1225 int __cil_tmp76 ;
1226 int __cil_tmp77 ;
1227 int __cil_tmp78 = __VERIFIER_nondet_int() ;
1228 int __cil_tmp79 ;
1229 int __cil_tmp80 ;
1230 int __cil_tmp81 = __VERIFIER_nondet_int() ;
1231 int __cil_tmp82 ;
1232 int __cil_tmp83 ;
1233 int __cil_tmp84 ;
1234 int __cil_tmp85 ;
1235 int __cil_tmp86 ;
1236 int __cil_tmp87 ;
1237 int __cil_tmp88 = __VERIFIER_nondet_int() ;
1238 int __cil_tmp89 ;
1239 int __cil_tmp90 ;
1240 long __cil_tmp91 ;
1241
1242 {
1243 if (disketteExtension__HoldNewRequests) {
1244 {
1245 //__cil_tmp39 = 3 << 14;
1246 //__cil_tmp40 = 50 << 16;
1247 //__cil_tmp41 = __cil_tmp40 | __cil_tmp39;
1248 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 != __cil_tmp41) {
1249 {
1250 ntStatus = FloppyQueueRequest(disketteExtension, Irp);
1251 }
1252 return (ntStatus);
1253 }
1254 }
1255 }
1256 if (disketteExtension__IsRemoved) {
1257 {
1258 Irp__IoStatus__Information = 0;
1259 Irp__IoStatus__Status___0 = -1073741738;
1260 myStatus = -1073741738;
1261 IofCompleteRequest(Irp, 0);
1262 }
1263 return (-1073741738);
1264 }
1265 if (! disketteExtension__IsStarted) {
1266 if (s == NP) {
1267 s = SKIP1;
1268 } else {
1269 {
1270 errorFn();
1271 }
1272 }
1273 {
1274 Irp__CurrentLocation ++;
1275 Irp__Tail__Overlay__CurrentStackLocation ++;
1276 tmp = IofCallDriver(disketteExtension__TargetObject, Irp);
1277 }
1278 return (tmp);
1279 }
1280 {
1281 //__cil_tmp42 = 2 << 2;
1282 //__cil_tmp43 = 77 << 16;
1283 //__cil_tmp44 = __cil_tmp43 | __cil_tmp42;
1284 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp44) {
1285 goto switch_13_exp_0;
1286 } else {
1287 {
1288 //__cil_tmp45 = 77 << 16;
1289 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp45) {
1290 goto switch_13_exp_1;
1291 } else {
1292 {
1293 //__cil_tmp46 = 6 << 2;
1294 //__cil_tmp47 = 3 << 14;
1295 //__cil_tmp48 = 7 << 16;
1296 //__cil_tmp49 = __cil_tmp48 | __cil_tmp47;
1297 //__cil_tmp50 = __cil_tmp49 | __cil_tmp46;
1298 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp50) {
1299 goto switch_13_exp_2;
1300 } else {
1301 {
1302 // __cil_tmp51 = 11 << 2;
1303 //__cil_tmp52 = 3 << 14;
1304 //__cil_tmp53 = 7 << 16;
1305 // __cil_tmp54 = __cil_tmp53 | __cil_tmp52;
1306 //__cil_tmp55 = __cil_tmp54 | __cil_tmp51;
1307 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp55) {
1308 goto switch_13_exp_3;
1309 } else {
1310 {
1311 // __cil_tmp56 = 512 << 2;
1312 // __cil_tmp57 = 1 << 14;
1313 // __cil_tmp58 = 7 << 16;
1314 //__cil_tmp59 = __cil_tmp58 | __cil_tmp57;
1315 // __cil_tmp60 = __cil_tmp59 | __cil_tmp56;
1316 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp60) {
1317 goto switch_13_exp_4;
1318 } else {
1319 {
1320 //__cil_tmp61 = 512 << 2;
1321 //__cil_tmp62 = 1 << 14;
1322 // __cil_tmp63 = 45 << 16;
1323 //__cil_tmp64 = __cil_tmp63 | __cil_tmp62;
1324 //__cil_tmp65 = __cil_tmp64 | __cil_tmp61;
1325 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp65) {
1326 goto switch_13_exp_5;
1327 } else {
1328 {
1329 //__cil_tmp66 = 7 << 16;
1330 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp66) {
1331 goto switch_13_exp_6;
1332 } else {
1333 {
1334 //__cil_tmp67 = 9 << 2;
1335 //__cil_tmp68 = 7 << 16;
1336 //__cil_tmp69 = __cil_tmp68 | __cil_tmp67;
1337 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp69) {
1338 goto switch_13_exp_7;
1339 } else {
1340 {
1341 //__cil_tmp70 = 768 << 2;
1342 //__cil_tmp71 = 7 << 16;
1343 //__cil_tmp72 = __cil_tmp71 | __cil_tmp70;
1344 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp72) {
1345 goto switch_13_exp_8;
1346 } else {
1347 {
1348 //__cil_tmp73 = 768 << 2;
1349 // __cil_tmp74 = 45 << 16;
1350 //__cil_tmp75 = __cil_tmp74 | __cil_tmp73;
1351 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp75) {
1352 goto switch_13_exp_9;
1353 } else {
1354 {
1355 //__cil_tmp76 = 3 << 2;
1356 //__cil_tmp77 = 77 << 16;
1357 //__cil_tmp78 = __cil_tmp77 | __cil_tmp76;
1358 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp78) {
1359 goto switch_13_exp_10;
1360 } else {
1361 {
1362 //__cil_tmp79 = 248 << 2;
1363 //__cil_tmp80 = 7 << 16;
1364 //__cil_tmp81 = __cil_tmp80 | __cil_tmp79;
1365 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp81) {
1366 goto switch_13_exp_11;
1367 } else {
1368 goto switch_13_default;
1369 if (0) {
1370 switch_13_exp_0: ;
1371 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < sizeof__MOUNTDEV_NAME) {
1372 ntStatus = -1073741811;
1373 goto switch_13_break;
1374 }
1375 mountName = Irp__AssociatedIrp__SystemBuffer;
1376 mountName__NameLength = disketteExtension__DeviceName__Length;
1377 {
1378 __cil_tmp82 = sizeof__USHORT + mountName__NameLength;
1379 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < __cil_tmp82) {
1380 ntStatus = -2147483643;
1381 Irp__IoStatus__Information = sizeof__MOUNTDEV_NAME;
1382 goto switch_13_break;
1383 }
1384 }
1385 ntStatus = 0;
1386 Irp__IoStatus__Information = sizeof__USHORT + mountName__NameLength;
1387 goto switch_13_break;
1388 switch_13_exp_1: ;
1389 if (! disketteExtension__InterfaceString__Buffer) {
1390 ntStatus = -1073741811;
1391 goto switch_13_break;
1392 } else {
1393 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < sizeof__MOUNTDEV_UNIQUE_ID) {
1394 ntStatus = -1073741811;
1395 goto switch_13_break;
1396 }
1397 }
1398 uniqueId = Irp__AssociatedIrp__SystemBuffer;
1399 uniqueId__UniqueIdLength = disketteExtension__InterfaceString__Length;
1400 {
1401 __cil_tmp83 = sizeof__USHORT + uniqueId__UniqueIdLength;
1402 if (irpSp__Parameters__DeviceIoControl__OutputBufferLength < __cil_tmp83) {
1403 ntStatus = -2147483643;
1404 Irp__IoStatus__Information = sizeof__MOUNTDEV_UNIQUE_ID;
1405 goto switch_13_break;
1406 }
1407 }
1408 ntStatus = 0;
1409 Irp__IoStatus__Information = sizeof__USHORT + uniqueId__UniqueIdLength;
1410 goto switch_13_break;
1411 switch_13_exp_2: ;
1412 switch_13_exp_3: ;
1413 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < sizeof__FORMAT_PARAMETERS) {
1414 ntStatus = -1073741811;
1415 goto switch_13_break;
1416 }
1417 {
1418 tmp___0 = FlCheckFormatParameters(disketteExtension, Irp__AssociatedIrp__SystemBuffer);
1419 }
1420 if (! tmp___0) {
1421 ntStatus = -1073741811;
1422 goto switch_13_break;
1423 }
1424 {
1425 //__cil_tmp84 = 11 << 2;
1426 //__cil_tmp85 = 3 << 14;
1427 //__cil_tmp86 = 7 << 16;
1428 //__cil_tmp87 = __cil_tmp86 | __cil_tmp85;
1429 //__cil_tmp88 = __cil_tmp87 | __cil_tmp84;
1430 if (irpSp__Parameters__DeviceIoControl__IoControlCode___1 == __cil_tmp88) {
1431 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < sizeof__FORMAT_EX_PARAMETERS) {
1432 ntStatus = -1073741811;
1433 goto switch_13_break;
1434 }
1435 formatExParameters = Irp__AssociatedIrp__SystemBuffer;
1436 if (irpSp__Parameters__DeviceIoControl__InputBufferLength < formatExParametersSize) {
1437 ntStatus = -1073741811;
1438 goto switch_13_break;
1439 } else {
1440 if (formatExParameters__FormatGapLength >= 256) {
1441 ntStatus = -1073741811;
1442 goto switch_13_break;
1443 } else {
1444 if (formatExParameters__SectorsPerTrack >= 256) {
1445 ntStatus = -1073741811;
1446 goto switch_13_break;
1447 }
1448 }
1449 }
1450 }
1451 }
1452 switch_13_exp_4: ;
1453 switch_13_exp_5: ;
1454 switch_13_exp_6: ;
1455 switch_13_exp_7:
1456 {
1457 ntStatus = FlQueueIrpToThread(Irp, disketteExtension);
1458 }
1459 goto switch_13_break;
1460 switch_13_exp_8: ;
1461 switch_13_exp_9:
1462 outputBufferLength = irpSp__Parameters__DeviceIoControl__OutputBufferLength;
1463 if (outputBufferLength < sizeof__DISK_GEOMETRY) {
1464 ntStatus = -1073741789;
1465 goto switch_13_break;
1466 }
1467 ntStatus = 0;
1468 {
1469 __cil_tmp89 = highestDriveMediaType - lowestDriveMediaType;
1470 __cil_tmp90 = __cil_tmp89 + 1;
1471 if (outputBufferLength < __cil_tmp90) {
1472 ntStatus = -2147483643;
1473 }
1474 }
1475 goto switch_13_break;
1476 switch_13_exp_10: ;
1477 switch_13_exp_11: ;
1478 switch_13_default: ;
1479 if (s == NP) {
1480 s = SKIP1;
1481 } else {
1482 {
1483 errorFn();
1484 }
1485 }
1486 {
1487 Irp__CurrentLocation ++;
1488 Irp__Tail__Overlay__CurrentStackLocation ++;
1489 ntStatus = IofCallDriver(disketteExtension__TargetObject,
1490 Irp);
1491 }
1492 return (ntStatus);
1493 } else {
1494 switch_13_break: ;
1495 }
1496 }
1497 }
1498 }
1499 }
1500 }
1501 }
1502 }
1503 }
1504 }
1505 }
1506 }
1507 }
1508 }
1509 }
1510 }
1511 }
1512 }
1513 }
1514 }
1515 }
1516 }
1517 }
1518 }
1519 }
1520 {
1521 __cil_tmp91 = (long )ntStatus;
1522 if (__cil_tmp91 != 259L) {
1523 {
1524 Irp__IoStatus__Status___0 = ntStatus;
1525 myStatus = ntStatus;
1526 IofCompleteRequest(Irp, 0);
1527 }
1528 }
1529 }
1530 return (ntStatus);
1531}
1532}
1533int FlCheckFormatParameters(int DisketteExtension , int FormatParameters )
1534{ int DriveMediaConstants__driveMediaType__MediaType = __VERIFIER_nondet_int() ;
1535 int FormatParameters__MediaType = __VERIFIER_nondet_int() ;
1536 int FAKE_CONDITION = __VERIFIER_nondet_int() ;
1537
1538 {
1539 if (DriveMediaConstants__driveMediaType__MediaType != FormatParameters__MediaType) {
1540 return (0);
1541 } else {
1542 if (FAKE_CONDITION) {
1543 return (0);
1544 } else {
1545 return (1);
1546 }
1547 }
1548}
1549}
1550int FloppyQueueRequest(int DisketteExtension , int Irp )
1551{ int Irp__IoStatus__Status ;
1552 int Irp__IoStatus__Information ;
1553 int Irp__Tail__Overlay__CurrentStackLocation__Control ;
1554 int ntStatus ;
1555 int FAKE_CONDITION = __VERIFIER_nondet_int() ;
1556
1557 {
1558 PagingReferenceCount ++;
1559 if (PagingReferenceCount == 1) {
1560
1561 }
1562 if (FAKE_CONDITION) {
1563 {
1564 Irp__IoStatus__Status = -1073741536;
1565 myStatus = -1073741536;
1566 Irp__IoStatus__Information = 0;
1567 IofCompleteRequest(Irp, 0);
1568 PagingReferenceCount --;
1569 }
1570 if (PagingReferenceCount == 0) {
1571
1572 }
1573 ntStatus = -1073741536;
1574 } else {
1575 Irp__IoStatus__Status = 259;
1576 myStatus = 259;
1577 //Irp__Tail__Overlay__CurrentStackLocation__Control |= 1;
1578 if (pended == 0) {
1579 pended = 1;
1580 } else {
1581 {
1582 errorFn();
1583 }
1584 }
1585 ntStatus = 259;
1586 }
1587 return (ntStatus);
1588}
1589}
1590
1591void errorFn(void)
1592{
1593
1594 {
1595 ERROR: __VERIFIER_error();
1596 return;
1597}
1598}
Note: See TracBrowser for help on using the repository browser.