Showing error 43

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ntdrivers-simplified/kbfiltr_simpl2.cil.c
Line in file: 1320
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

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