Showing error 1645

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/elevator_spec3_product27_unsafe.cil.c
Line in file: 4961
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

   1extern int __VERIFIER_nondet_int(void);
   2/* Generated by CIL v. 1.3.7 */
   3/* print_CIL_Input is true */
   4
   5#line 2 "libacc.c"
   6struct JoinPoint {
   7   void **(*fp)(struct JoinPoint * ) ;
   8   void **args ;
   9   int argsCount ;
  10   char const   **argsType ;
  11   void *(*arg)(int  , struct JoinPoint * ) ;
  12   char const   *(*argType)(int  , struct JoinPoint * ) ;
  13   void **retValue ;
  14   char const   *retType ;
  15   char const   *funcName ;
  16   char const   *targetName ;
  17   char const   *fileName ;
  18   char const   *kind ;
  19   void *excep_return ;
  20};
  21#line 18 "libacc.c"
  22struct __UTAC__CFLOW_FUNC {
  23   int (*func)(int  , int  ) ;
  24   int val ;
  25   struct __UTAC__CFLOW_FUNC *next ;
  26};
  27#line 18 "libacc.c"
  28struct __UTAC__EXCEPTION {
  29   void *jumpbuf ;
  30   unsigned long long prtValue ;
  31   int pops ;
  32   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  33};
  34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  35typedef unsigned long size_t;
  36#line 76 "libacc.c"
  37struct __ACC__ERR {
  38   void *v ;
  39   struct __ACC__ERR *next ;
  40};
  41#line 1 "Elevator.o"
  42#pragma merger(0,"Elevator.i","")
  43#line 359 "/usr/include/stdio.h"
  44extern int printf(char const   * __restrict  __format  , ...) ;
  45#line 10 "Person.h"
  46int getWeight(int person ) ;
  47#line 14
  48int getDestination(int person ) ;
  49#line 16
  50void enterElevator(int p ) ;
  51#line 12 "Floor.h"
  52int isFloorCalling(int floorID ) ;
  53#line 14
  54void resetCallOnFloor(int floorID ) ;
  55#line 18
  56int isPersonOnFloor(int person , int floor ) ;
  57#line 22
  58void removePersonFromFloor(int person , int floor ) ;
  59#line 24
  60int isTopFloor(int floorID ) ;
  61#line 28
  62void initFloors(void) ;
  63#line 20 "Elevator.h"
  64void timeShift(void) ;
  65#line 22
  66int isBlocked(void) ;
  67#line 24
  68void printState(void) ;
  69#line 26
  70int isEmpty(void) ;
  71#line 28
  72int isAnyLiftButtonPressed(void) ;
  73#line 30
  74int buttonForFloorIsPressed(int floorID ) ;
  75#line 33
  76void initTopDown(void) ;
  77#line 35
  78void initBottomUp(void) ;
  79#line 38
  80int areDoorsOpen(void) ;
  81#line 40
  82int getCurrentFloorID(void) ;
  83#line 42
  84int isIdle(void) ;
  85#line 45 "Elevator.h"
  86int weight  =    0;
  87#line 47 "Elevator.h"
  88int maximumWeight  =    100;
  89#line 55 "Elevator.h"
  90int executiveFloor  =    4;
  91#line 58
  92int isExecutiveFloorCalling(void) ;
  93#line 60
  94int isExecutiveFloor(int floorID ) ;
  95#line 16 "Elevator.c"
  96int currentHeading  =    1;
  97#line 18 "Elevator.c"
  98int currentFloorID  =    0;
  99#line 20 "Elevator.c"
 100int persons_0  ;
 101#line 22 "Elevator.c"
 102int persons_1  ;
 103#line 24 "Elevator.c"
 104int persons_2  ;
 105#line 26 "Elevator.c"
 106int persons_3  ;
 107#line 28 "Elevator.c"
 108int persons_4  ;
 109#line 30 "Elevator.c"
 110int persons_5  ;
 111#line 33 "Elevator.c"
 112int doorState  =    1;
 113#line 35 "Elevator.c"
 114int floorButtons_0  ;
 115#line 37 "Elevator.c"
 116int floorButtons_1  ;
 117#line 39 "Elevator.c"
 118int floorButtons_2  ;
 119#line 41 "Elevator.c"
 120int floorButtons_3  ;
 121#line 43 "Elevator.c"
 122int floorButtons_4  ;
 123#line 51 "Elevator.c"
 124void initTopDown(void) 
 125{ 
 126
 127  {
 128  {
 129#line 52
 130  currentFloorID = 4;
 131#line 53
 132  currentHeading = 0;
 133#line 54
 134  floorButtons_0 = 0;
 135#line 55
 136  floorButtons_1 = 0;
 137#line 56
 138  floorButtons_2 = 0;
 139#line 57
 140  floorButtons_3 = 0;
 141#line 58
 142  floorButtons_4 = 0;
 143#line 59
 144  persons_0 = 0;
 145#line 60
 146  persons_1 = 0;
 147#line 61
 148  persons_2 = 0;
 149#line 62
 150  persons_3 = 0;
 151#line 63
 152  persons_4 = 0;
 153#line 64
 154  persons_5 = 0;
 155#line 65
 156  initFloors();
 157  }
 158#line 1081 "Elevator.c"
 159  return;
 160}
 161}
 162#line 68 "Elevator.c"
 163void initBottomUp(void) 
 164{ 
 165
 166  {
 167  {
 168#line 69
 169  currentFloorID = 0;
 170#line 70
 171  currentHeading = 1;
 172#line 71
 173  floorButtons_0 = 0;
 174#line 72
 175  floorButtons_1 = 0;
 176#line 73
 177  floorButtons_2 = 0;
 178#line 74
 179  floorButtons_3 = 0;
 180#line 75
 181  floorButtons_4 = 0;
 182#line 76
 183  persons_0 = 0;
 184#line 77
 185  persons_1 = 0;
 186#line 78
 187  persons_2 = 0;
 188#line 79
 189  persons_3 = 0;
 190#line 80
 191  persons_4 = 0;
 192#line 81
 193  persons_5 = 0;
 194#line 82
 195  initFloors();
 196  }
 197#line 1127 "Elevator.c"
 198  return;
 199}
 200}
 201#line 86 "Elevator.c"
 202int isBlocked(void) 
 203{ int retValue_acc ;
 204
 205  {
 206#line 1145 "Elevator.c"
 207  retValue_acc = 0;
 208#line 1147
 209  return (retValue_acc);
 210#line 1154
 211  return (retValue_acc);
 212}
 213}
 214#line 91 "Elevator.c"
 215void enterElevator__wrappee__base(int p ) 
 216{ 
 217
 218  {
 219#line 100
 220  if (p == 0) {
 221#line 101
 222    persons_0 = 1;
 223  } else {
 224#line 102
 225    if (p == 1) {
 226#line 103
 227      persons_1 = 1;
 228    } else {
 229#line 104
 230      if (p == 2) {
 231#line 105
 232        persons_2 = 1;
 233      } else {
 234#line 106
 235        if (p == 3) {
 236#line 107
 237          persons_3 = 1;
 238        } else {
 239#line 108
 240          if (p == 4) {
 241#line 109
 242            persons_4 = 1;
 243          } else {
 244#line 110
 245            if (p == 5) {
 246#line 111
 247              persons_5 = 1;
 248            } else {
 249
 250            }
 251          }
 252        }
 253      }
 254    }
 255  }
 256#line 1189 "Elevator.c"
 257  return;
 258}
 259}
 260#line 102 "Elevator.c"
 261void enterElevator(int p ) 
 262{ int tmp ;
 263
 264  {
 265  {
 266#line 103
 267  enterElevator__wrappee__base(p);
 268#line 104
 269  tmp = getWeight(p);
 270#line 104
 271  weight = weight + tmp;
 272  }
 273#line 1211 "Elevator.c"
 274  return;
 275}
 276}
 277#line 107 "Elevator.c"
 278void leaveElevator__wrappee__base(int p ) 
 279{ 
 280
 281  {
 282#line 115
 283  if (p == 0) {
 284#line 116
 285    persons_0 = 0;
 286  } else {
 287#line 117
 288    if (p == 1) {
 289#line 118
 290      persons_1 = 0;
 291    } else {
 292#line 119
 293      if (p == 2) {
 294#line 120
 295        persons_2 = 0;
 296      } else {
 297#line 121
 298        if (p == 3) {
 299#line 122
 300          persons_3 = 0;
 301        } else {
 302#line 123
 303          if (p == 4) {
 304#line 124
 305            persons_4 = 0;
 306          } else {
 307#line 125
 308            if (p == 5) {
 309#line 126
 310              persons_5 = 0;
 311            } else {
 312
 313            }
 314          }
 315        }
 316      }
 317    }
 318  }
 319#line 1242 "Elevator.c"
 320  return;
 321}
 322}
 323#line 117 "Elevator.c"
 324void leaveElevator__wrappee__weight(int p ) 
 325{ int tmp ;
 326
 327  {
 328  {
 329#line 118
 330  leaveElevator__wrappee__base(p);
 331#line 119
 332  tmp = getWeight(p);
 333#line 119
 334  weight = weight - tmp;
 335  }
 336#line 1264 "Elevator.c"
 337  return;
 338}
 339}
 340#line 123 "Elevator.c"
 341void leaveElevator(int p ) 
 342{ int tmp ;
 343
 344  {
 345  {
 346#line 124
 347  leaveElevator__wrappee__weight(p);
 348#line 126
 349  tmp = isEmpty();
 350  }
 351#line 126
 352  if (tmp) {
 353#line 127
 354    floorButtons_0 = 0;
 355#line 128
 356    floorButtons_1 = 0;
 357#line 129
 358    floorButtons_2 = 0;
 359#line 130
 360    floorButtons_3 = 0;
 361#line 131
 362    floorButtons_4 = 0;
 363  } else {
 364
 365  }
 366#line 1297 "Elevator.c"
 367  return;
 368}
 369}
 370#line 135 "Elevator.c"
 371void pressInLiftFloorButton(int floorID ) 
 372{ 
 373
 374  {
 375#line 141
 376  if (floorID == 0) {
 377#line 142
 378    floorButtons_0 = 1;
 379  } else {
 380#line 143
 381    if (floorID == 1) {
 382#line 144
 383      floorButtons_1 = 1;
 384    } else {
 385#line 145
 386      if (floorID == 2) {
 387#line 146
 388        floorButtons_2 = 1;
 389      } else {
 390#line 147
 391        if (floorID == 3) {
 392#line 148
 393          floorButtons_3 = 1;
 394        } else {
 395#line 149
 396          if (floorID == 4) {
 397#line 150
 398            floorButtons_4 = 1;
 399          } else {
 400
 401          }
 402        }
 403      }
 404    }
 405  }
 406#line 1326 "Elevator.c"
 407  return;
 408}
 409}
 410#line 143 "Elevator.c"
 411void resetFloorButton(int floorID ) 
 412{ 
 413
 414  {
 415#line 149
 416  if (floorID == 0) {
 417#line 150
 418    floorButtons_0 = 0;
 419  } else {
 420#line 151
 421    if (floorID == 1) {
 422#line 152
 423      floorButtons_1 = 0;
 424    } else {
 425#line 153
 426      if (floorID == 2) {
 427#line 154
 428        floorButtons_2 = 0;
 429      } else {
 430#line 155
 431        if (floorID == 3) {
 432#line 156
 433          floorButtons_3 = 0;
 434        } else {
 435#line 157
 436          if (floorID == 4) {
 437#line 158
 438            floorButtons_4 = 0;
 439          } else {
 440
 441          }
 442        }
 443      }
 444    }
 445  }
 446#line 1355 "Elevator.c"
 447  return;
 448}
 449}
 450#line 151 "Elevator.c"
 451int getCurrentFloorID(void) 
 452{ int retValue_acc ;
 453
 454  {
 455#line 1373 "Elevator.c"
 456  retValue_acc = currentFloorID;
 457#line 1375
 458  return (retValue_acc);
 459#line 1382
 460  return (retValue_acc);
 461}
 462}
 463#line 155 "Elevator.c"
 464int areDoorsOpen(void) 
 465{ int retValue_acc ;
 466
 467  {
 468#line 1404 "Elevator.c"
 469  retValue_acc = doorState;
 470#line 1406
 471  return (retValue_acc);
 472#line 1413
 473  return (retValue_acc);
 474}
 475}
 476#line 159 "Elevator.c"
 477int buttonForFloorIsPressed(int floorID ) 
 478{ int retValue_acc ;
 479
 480  {
 481#line 165 "Elevator.c"
 482  if (floorID == 0) {
 483#line 1436
 484    retValue_acc = floorButtons_0;
 485#line 1438
 486    return (retValue_acc);
 487  } else {
 488#line 1440
 489    if (floorID == 1) {
 490#line 1443
 491      retValue_acc = floorButtons_1;
 492#line 1445
 493      return (retValue_acc);
 494    } else {
 495#line 1447
 496      if (floorID == 2) {
 497#line 1450
 498        retValue_acc = floorButtons_2;
 499#line 1452
 500        return (retValue_acc);
 501      } else {
 502#line 1454
 503        if (floorID == 3) {
 504#line 1457
 505          retValue_acc = floorButtons_3;
 506#line 1459
 507          return (retValue_acc);
 508        } else {
 509#line 1461
 510          if (floorID == 4) {
 511#line 1464
 512            retValue_acc = floorButtons_4;
 513#line 1466
 514            return (retValue_acc);
 515          } else {
 516#line 1470 "Elevator.c"
 517            retValue_acc = 0;
 518#line 1472
 519            return (retValue_acc);
 520          }
 521        }
 522      }
 523    }
 524  }
 525#line 1479 "Elevator.c"
 526  return (retValue_acc);
 527}
 528}
 529#line 168 "Elevator.c"
 530int getCurrentHeading(void) 
 531{ int retValue_acc ;
 532
 533  {
 534#line 1501 "Elevator.c"
 535  retValue_acc = currentHeading;
 536#line 1503
 537  return (retValue_acc);
 538#line 1510
 539  return (retValue_acc);
 540}
 541}
 542#line 172 "Elevator.c"
 543int isEmpty(void) 
 544{ int retValue_acc ;
 545
 546  {
 547#line 179 "Elevator.c"
 548  if (persons_0 == 1) {
 549#line 1533
 550    retValue_acc = 0;
 551#line 1535
 552    return (retValue_acc);
 553  } else {
 554#line 1537
 555    if (persons_1 == 1) {
 556#line 1540
 557      retValue_acc = 0;
 558#line 1542
 559      return (retValue_acc);
 560    } else {
 561#line 1544
 562      if (persons_2 == 1) {
 563#line 1547
 564        retValue_acc = 0;
 565#line 1549
 566        return (retValue_acc);
 567      } else {
 568#line 1551
 569        if (persons_3 == 1) {
 570#line 1554
 571          retValue_acc = 0;
 572#line 1556
 573          return (retValue_acc);
 574        } else {
 575#line 1558
 576          if (persons_4 == 1) {
 577#line 1561
 578            retValue_acc = 0;
 579#line 1563
 580            return (retValue_acc);
 581          } else {
 582#line 1565
 583            if (persons_5 == 1) {
 584#line 1568 "Elevator.c"
 585              retValue_acc = 0;
 586#line 1570
 587              return (retValue_acc);
 588            } else {
 589
 590            }
 591          }
 592        }
 593      }
 594    }
 595  }
 596#line 1575 "Elevator.c"
 597  retValue_acc = 1;
 598#line 1577
 599  return (retValue_acc);
 600#line 1584
 601  return (retValue_acc);
 602}
 603}
 604#line 183 "Elevator.c"
 605int anyStopRequested(void) 
 606{ int retValue_acc ;
 607  int tmp ;
 608  int tmp___0 ;
 609  int tmp___1 ;
 610  int tmp___2 ;
 611  int tmp___3 ;
 612
 613  {
 614  {
 615#line 194
 616  tmp___3 = isFloorCalling(0);
 617  }
 618#line 194 "Elevator.c"
 619  if (tmp___3) {
 620#line 1607
 621    retValue_acc = 1;
 622#line 1609
 623    return (retValue_acc);
 624  } else {
 625#line 1611
 626    if (floorButtons_0) {
 627#line 1614
 628      retValue_acc = 1;
 629#line 1616
 630      return (retValue_acc);
 631    } else {
 632      {
 633#line 1618 "Elevator.c"
 634      tmp___2 = isFloorCalling(1);
 635      }
 636#line 1618
 637      if (tmp___2) {
 638#line 1621
 639        retValue_acc = 1;
 640#line 1623
 641        return (retValue_acc);
 642      } else {
 643#line 1625
 644        if (floorButtons_1) {
 645#line 1628
 646          retValue_acc = 1;
 647#line 1630
 648          return (retValue_acc);
 649        } else {
 650          {
 651#line 1632
 652          tmp___1 = isFloorCalling(2);
 653          }
 654#line 1632
 655          if (tmp___1) {
 656#line 1635
 657            retValue_acc = 1;
 658#line 1637
 659            return (retValue_acc);
 660          } else {
 661#line 1639
 662            if (floorButtons_2) {
 663#line 1642
 664              retValue_acc = 1;
 665#line 1644
 666              return (retValue_acc);
 667            } else {
 668              {
 669#line 1646
 670              tmp___0 = isFloorCalling(3);
 671              }
 672#line 1646
 673              if (tmp___0) {
 674#line 1649
 675                retValue_acc = 1;
 676#line 1651
 677                return (retValue_acc);
 678              } else {
 679#line 1653
 680                if (floorButtons_3) {
 681#line 1656
 682                  retValue_acc = 1;
 683#line 1658
 684                  return (retValue_acc);
 685                } else {
 686                  {
 687#line 1660
 688                  tmp = isFloorCalling(4);
 689                  }
 690#line 1660
 691                  if (tmp) {
 692#line 1663
 693                    retValue_acc = 1;
 694#line 1665
 695                    return (retValue_acc);
 696                  } else {
 697#line 1667
 698                    if (floorButtons_4) {
 699#line 1670
 700                      retValue_acc = 1;
 701#line 1672
 702                      return (retValue_acc);
 703                    } else {
 704
 705                    }
 706                  }
 707                }
 708              }
 709            }
 710          }
 711        }
 712      }
 713    }
 714  }
 715#line 1677 "Elevator.c"
 716  retValue_acc = 0;
 717#line 1679
 718  return (retValue_acc);
 719#line 1686
 720  return (retValue_acc);
 721}
 722}
 723#line 197 "Elevator.c"
 724int isIdle(void) 
 725{ int retValue_acc ;
 726  int tmp ;
 727
 728  {
 729  {
 730#line 1708 "Elevator.c"
 731  tmp = anyStopRequested();
 732#line 1708
 733  retValue_acc = tmp == 0;
 734  }
 735#line 1710
 736  return (retValue_acc);
 737#line 1717
 738  return (retValue_acc);
 739}
 740}
 741#line 201 "Elevator.c"
 742int stopRequestedInDirection__wrappee__empty(int dir , int respectFloorCalls , int respectInLiftCalls ) 
 743{ int retValue_acc ;
 744  int tmp ;
 745  int tmp___0 ;
 746  int tmp___1 ;
 747  int tmp___2 ;
 748  int tmp___3 ;
 749  int tmp___4 ;
 750  int tmp___5 ;
 751  int tmp___6 ;
 752  int tmp___7 ;
 753  int tmp___8 ;
 754  int tmp___9 ;
 755
 756  {
 757#line 252
 758  if (dir == 1) {
 759    {
 760#line 212
 761    tmp = isTopFloor(currentFloorID);
 762    }
 763#line 212 "Elevator.c"
 764    if (tmp) {
 765#line 1743 "Elevator.c"
 766      retValue_acc = 0;
 767#line 1745
 768      return (retValue_acc);
 769    } else {
 770
 771    }
 772#line 212
 773    if (currentFloorID < 0) {
 774#line 212
 775      if (respectFloorCalls) {
 776        {
 777#line 212 "Elevator.c"
 778        tmp___4 = isFloorCalling(0);
 779        }
 780#line 212 "Elevator.c"
 781        if (tmp___4) {
 782#line 1751 "Elevator.c"
 783          retValue_acc = 1;
 784#line 1753
 785          return (retValue_acc);
 786        } else {
 787          goto _L___16;
 788        }
 789      } else {
 790        goto _L___16;
 791      }
 792    } else {
 793      _L___16: /* CIL Label */ 
 794#line 1755
 795      if (currentFloorID < 0) {
 796#line 1755
 797        if (respectInLiftCalls) {
 798#line 1755
 799          if (floorButtons_0) {
 800#line 1758
 801            retValue_acc = 1;
 802#line 1760
 803            return (retValue_acc);
 804          } else {
 805            goto _L___14;
 806          }
 807        } else {
 808          goto _L___14;
 809        }
 810      } else {
 811        _L___14: /* CIL Label */ 
 812#line 1762
 813        if (currentFloorID < 1) {
 814#line 1762
 815          if (respectFloorCalls) {
 816            {
 817#line 1762
 818            tmp___3 = isFloorCalling(1);
 819            }
 820#line 1762
 821            if (tmp___3) {
 822#line 1765
 823              retValue_acc = 1;
 824#line 1767
 825              return (retValue_acc);
 826            } else {
 827              goto _L___12;
 828            }
 829          } else {
 830            goto _L___12;
 831          }
 832        } else {
 833          _L___12: /* CIL Label */ 
 834#line 1769
 835          if (currentFloorID < 1) {
 836#line 1769
 837            if (respectInLiftCalls) {
 838#line 1769
 839              if (floorButtons_1) {
 840#line 1772
 841                retValue_acc = 1;
 842#line 1774
 843                return (retValue_acc);
 844              } else {
 845                goto _L___10;
 846              }
 847            } else {
 848              goto _L___10;
 849            }
 850          } else {
 851            _L___10: /* CIL Label */ 
 852#line 1776
 853            if (currentFloorID < 2) {
 854#line 1776
 855              if (respectFloorCalls) {
 856                {
 857#line 1776
 858                tmp___2 = isFloorCalling(2);
 859                }
 860#line 1776
 861                if (tmp___2) {
 862#line 1779
 863                  retValue_acc = 1;
 864#line 1781
 865                  return (retValue_acc);
 866                } else {
 867                  goto _L___8;
 868                }
 869              } else {
 870                goto _L___8;
 871              }
 872            } else {
 873              _L___8: /* CIL Label */ 
 874#line 1783
 875              if (currentFloorID < 2) {
 876#line 1783
 877                if (respectInLiftCalls) {
 878#line 1783
 879                  if (floorButtons_2) {
 880#line 1786
 881                    retValue_acc = 1;
 882#line 1788
 883                    return (retValue_acc);
 884                  } else {
 885                    goto _L___6;
 886                  }
 887                } else {
 888                  goto _L___6;
 889                }
 890              } else {
 891                _L___6: /* CIL Label */ 
 892#line 1790
 893                if (currentFloorID < 3) {
 894#line 1790
 895                  if (respectFloorCalls) {
 896                    {
 897#line 1790
 898                    tmp___1 = isFloorCalling(3);
 899                    }
 900#line 1790
 901                    if (tmp___1) {
 902#line 1793
 903                      retValue_acc = 1;
 904#line 1795
 905                      return (retValue_acc);
 906                    } else {
 907                      goto _L___4;
 908                    }
 909                  } else {
 910                    goto _L___4;
 911                  }
 912                } else {
 913                  _L___4: /* CIL Label */ 
 914#line 1797
 915                  if (currentFloorID < 3) {
 916#line 1797
 917                    if (respectInLiftCalls) {
 918#line 1797
 919                      if (floorButtons_3) {
 920#line 1800
 921                        retValue_acc = 1;
 922#line 1802
 923                        return (retValue_acc);
 924                      } else {
 925                        goto _L___2;
 926                      }
 927                    } else {
 928                      goto _L___2;
 929                    }
 930                  } else {
 931                    _L___2: /* CIL Label */ 
 932#line 1804
 933                    if (currentFloorID < 4) {
 934#line 1804
 935                      if (respectFloorCalls) {
 936                        {
 937#line 1804
 938                        tmp___0 = isFloorCalling(4);
 939                        }
 940#line 1804
 941                        if (tmp___0) {
 942#line 1807
 943                          retValue_acc = 1;
 944#line 1809
 945                          return (retValue_acc);
 946                        } else {
 947                          goto _L___0;
 948                        }
 949                      } else {
 950                        goto _L___0;
 951                      }
 952                    } else {
 953                      _L___0: /* CIL Label */ 
 954#line 1811
 955                      if (currentFloorID < 4) {
 956#line 1811
 957                        if (respectInLiftCalls) {
 958#line 1811
 959                          if (floorButtons_4) {
 960#line 1814
 961                            retValue_acc = 1;
 962#line 1816
 963                            return (retValue_acc);
 964                          } else {
 965#line 1820
 966                            retValue_acc = 0;
 967#line 1822
 968                            return (retValue_acc);
 969                          }
 970                        } else {
 971#line 1820
 972                          retValue_acc = 0;
 973#line 1822
 974                          return (retValue_acc);
 975                        }
 976                      } else {
 977#line 1820 "Elevator.c"
 978                        retValue_acc = 0;
 979#line 1822
 980                        return (retValue_acc);
 981                      }
 982                    }
 983                  }
 984                }
 985              }
 986            }
 987          }
 988        }
 989      }
 990    }
 991  } else {
 992#line 237 "Elevator.c"
 993    if (currentFloorID == 0) {
 994#line 1830 "Elevator.c"
 995      retValue_acc = 0;
 996#line 1832
 997      return (retValue_acc);
 998    } else {
 999
1000    }
1001#line 237
1002    if (currentFloorID > 0) {
1003#line 237
1004      if (respectFloorCalls) {
1005        {
1006#line 237 "Elevator.c"
1007        tmp___9 = isFloorCalling(0);
1008        }
1009#line 237 "Elevator.c"
1010        if (tmp___9) {
1011#line 1838 "Elevator.c"
1012          retValue_acc = 1;
1013#line 1840
1014          return (retValue_acc);
1015        } else {
1016          goto _L___34;
1017        }
1018      } else {
1019        goto _L___34;
1020      }
1021    } else {
1022      _L___34: /* CIL Label */ 
1023#line 1842
1024      if (currentFloorID > 0) {
1025#line 1842
1026        if (respectInLiftCalls) {
1027#line 1842
1028          if (floorButtons_0) {
1029#line 1845
1030            retValue_acc = 1;
1031#line 1847
1032            return (retValue_acc);
1033          } else {
1034            goto _L___32;
1035          }
1036        } else {
1037          goto _L___32;
1038        }
1039      } else {
1040        _L___32: /* CIL Label */ 
1041#line 1849
1042        if (currentFloorID > 1) {
1043#line 1849
1044          if (respectFloorCalls) {
1045            {
1046#line 1849
1047            tmp___8 = isFloorCalling(1);
1048            }
1049#line 1849
1050            if (tmp___8) {
1051#line 1852
1052              retValue_acc = 1;
1053#line 1854
1054              return (retValue_acc);
1055            } else {
1056              goto _L___30;
1057            }
1058          } else {
1059            goto _L___30;
1060          }
1061        } else {
1062          _L___30: /* CIL Label */ 
1063#line 1856
1064          if (currentFloorID > 1) {
1065#line 1856
1066            if (respectInLiftCalls) {
1067#line 1856
1068              if (floorButtons_1) {
1069#line 1859
1070                retValue_acc = 1;
1071#line 1861
1072                return (retValue_acc);
1073              } else {
1074                goto _L___28;
1075              }
1076            } else {
1077              goto _L___28;
1078            }
1079          } else {
1080            _L___28: /* CIL Label */ 
1081#line 1863
1082            if (currentFloorID > 2) {
1083#line 1863
1084              if (respectFloorCalls) {
1085                {
1086#line 1863
1087                tmp___7 = isFloorCalling(2);
1088                }
1089#line 1863
1090                if (tmp___7) {
1091#line 1866
1092                  retValue_acc = 1;
1093#line 1868
1094                  return (retValue_acc);
1095                } else {
1096                  goto _L___26;
1097                }
1098              } else {
1099                goto _L___26;
1100              }
1101            } else {
1102              _L___26: /* CIL Label */ 
1103#line 1870
1104              if (currentFloorID > 2) {
1105#line 1870
1106                if (respectInLiftCalls) {
1107#line 1870
1108                  if (floorButtons_2) {
1109#line 1873
1110                    retValue_acc = 1;
1111#line 1875
1112                    return (retValue_acc);
1113                  } else {
1114                    goto _L___24;
1115                  }
1116                } else {
1117                  goto _L___24;
1118                }
1119              } else {
1120                _L___24: /* CIL Label */ 
1121#line 1877
1122                if (currentFloorID > 3) {
1123#line 1877
1124                  if (respectFloorCalls) {
1125                    {
1126#line 1877
1127                    tmp___6 = isFloorCalling(3);
1128                    }
1129#line 1877
1130                    if (tmp___6) {
1131#line 1880
1132                      retValue_acc = 1;
1133#line 1882
1134                      return (retValue_acc);
1135                    } else {
1136                      goto _L___22;
1137                    }
1138                  } else {
1139                    goto _L___22;
1140                  }
1141                } else {
1142                  _L___22: /* CIL Label */ 
1143#line 1884
1144                  if (currentFloorID > 3) {
1145#line 1884
1146                    if (respectInLiftCalls) {
1147#line 1884
1148                      if (floorButtons_3) {
1149#line 1887
1150                        retValue_acc = 1;
1151#line 1889
1152                        return (retValue_acc);
1153                      } else {
1154                        goto _L___20;
1155                      }
1156                    } else {
1157                      goto _L___20;
1158                    }
1159                  } else {
1160                    _L___20: /* CIL Label */ 
1161#line 1891
1162                    if (currentFloorID > 4) {
1163#line 1891
1164                      if (respectFloorCalls) {
1165                        {
1166#line 1891
1167                        tmp___5 = isFloorCalling(4);
1168                        }
1169#line 1891
1170                        if (tmp___5) {
1171#line 1894
1172                          retValue_acc = 1;
1173#line 1896
1174                          return (retValue_acc);
1175                        } else {
1176                          goto _L___18;
1177                        }
1178                      } else {
1179                        goto _L___18;
1180                      }
1181                    } else {
1182                      _L___18: /* CIL Label */ 
1183#line 1898
1184                      if (currentFloorID > 4) {
1185#line 1898
1186                        if (respectInLiftCalls) {
1187#line 1898
1188                          if (floorButtons_4) {
1189#line 1901
1190                            retValue_acc = 1;
1191#line 1903
1192                            return (retValue_acc);
1193                          } else {
1194#line 1907
1195                            retValue_acc = 0;
1196#line 1909
1197                            return (retValue_acc);
1198                          }
1199                        } else {
1200#line 1907
1201                          retValue_acc = 0;
1202#line 1909
1203                          return (retValue_acc);
1204                        }
1205                      } else {
1206#line 1907 "Elevator.c"
1207                        retValue_acc = 0;
1208#line 1909
1209                        return (retValue_acc);
1210                      }
1211                    }
1212                  }
1213                }
1214              }
1215            }
1216          }
1217        }
1218      }
1219    }
1220  }
1221#line 1916 "Elevator.c"
1222  return (retValue_acc);
1223}
1224}
1225#line 256 "Elevator.c"
1226int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls ) 
1227{ int retValue_acc ;
1228  int tmp ;
1229  int tmp___0 ;
1230  int __cil_tmp7 ;
1231  int __cil_tmp8 ;
1232
1233  {
1234  {
1235#line 261
1236  tmp___0 = isExecutiveFloorCalling();
1237  }
1238#line 261 "Elevator.c"
1239  if (tmp___0) {
1240    {
1241#line 1941
1242    tmp = getCurrentFloorID();
1243#line 1941
1244    __cil_tmp7 = dir == 1;
1245#line 1941
1246    __cil_tmp8 = tmp < executiveFloor;
1247#line 1941
1248    retValue_acc = __cil_tmp8 == __cil_tmp7;
1249    }
1250#line 1943
1251    return (retValue_acc);
1252  } else {
1253    {
1254#line 1949 "Elevator.c"
1255    retValue_acc = stopRequestedInDirection__wrappee__empty(dir, respectFloorCalls,
1256                                                            respectInLiftCalls);
1257    }
1258#line 1951
1259    return (retValue_acc);
1260  }
1261#line 1958 "Elevator.c"
1262  return (retValue_acc);
1263}
1264}
1265#line 264 "Elevator.c"
1266int isAnyLiftButtonPressed(void) 
1267{ int retValue_acc ;
1268
1269  {
1270#line 270 "Elevator.c"
1271  if (floorButtons_0) {
1272#line 1981
1273    retValue_acc = 1;
1274#line 1983
1275    return (retValue_acc);
1276  } else {
1277#line 1985
1278    if (floorButtons_1) {
1279#line 1988
1280      retValue_acc = 1;
1281#line 1990
1282      return (retValue_acc);
1283    } else {
1284#line 1992
1285      if (floorButtons_2) {
1286#line 1995
1287        retValue_acc = 1;
1288#line 1997
1289        return (retValue_acc);
1290      } else {
1291#line 1999
1292        if (floorButtons_3) {
1293#line 2002
1294          retValue_acc = 1;
1295#line 2004
1296          return (retValue_acc);
1297        } else {
1298#line 2006
1299          if (floorButtons_4) {
1300#line 2009
1301            retValue_acc = 1;
1302#line 2011
1303            return (retValue_acc);
1304          } else {
1305#line 2015 "Elevator.c"
1306            retValue_acc = 0;
1307#line 2017
1308            return (retValue_acc);
1309          }
1310        }
1311      }
1312    }
1313  }
1314#line 2024 "Elevator.c"
1315  return (retValue_acc);
1316}
1317}
1318#line 273 "Elevator.c"
1319void continueInDirection(int dir ) 
1320{ int tmp ;
1321
1322  {
1323#line 274
1324  currentHeading = dir;
1325#line 275
1326  if (currentHeading == 1) {
1327    {
1328#line 280
1329    tmp = isTopFloor(currentFloorID);
1330    }
1331#line 280
1332    if (tmp) {
1333#line 278
1334      currentHeading = 0;
1335    } else {
1336
1337    }
1338  } else {
1339#line 285
1340    if (currentFloorID == 0) {
1341#line 283
1342      currentHeading = 1;
1343    } else {
1344
1345    }
1346  }
1347#line 286
1348  if (currentHeading == 1) {
1349#line 287
1350    currentFloorID = currentFloorID + 1;
1351  } else {
1352#line 289
1353    currentFloorID = currentFloorID - 1;
1354  }
1355#line 2070 "Elevator.c"
1356  return;
1357}
1358}
1359#line 293 "Elevator.c"
1360int stopRequestedAtCurrentFloor__wrappee__empty(void) 
1361{ int retValue_acc ;
1362  int tmp ;
1363  int tmp___0 ;
1364
1365  {
1366  {
1367#line 300
1368  tmp___0 = isFloorCalling(currentFloorID);
1369  }
1370#line 300 "Elevator.c"
1371  if (tmp___0) {
1372#line 2091
1373    retValue_acc = 1;
1374#line 2093
1375    return (retValue_acc);
1376  } else {
1377    {
1378#line 2095 "Elevator.c"
1379    tmp = buttonForFloorIsPressed(currentFloorID);
1380    }
1381#line 2095
1382    if (tmp) {
1383#line 2100
1384      retValue_acc = 1;
1385#line 2102
1386      return (retValue_acc);
1387    } else {
1388#line 2108
1389      retValue_acc = 0;
1390#line 2110
1391      return (retValue_acc);
1392    }
1393  }
1394#line 2117 "Elevator.c"
1395  return (retValue_acc);
1396}
1397}
1398#line 304 "Elevator.c"
1399int stopRequestedAtCurrentFloor(void) 
1400{ int retValue_acc ;
1401  int tmp ;
1402  int tmp___0 ;
1403
1404  {
1405  {
1406#line 307
1407  tmp = isExecutiveFloorCalling();
1408  }
1409#line 307
1410  if (tmp) {
1411    {
1412#line 307 "Elevator.c"
1413    tmp___0 = getCurrentFloorID();
1414    }
1415#line 307 "Elevator.c"
1416    if (executiveFloor == tmp___0) {
1417      {
1418#line 2148
1419      retValue_acc = stopRequestedAtCurrentFloor__wrappee__empty();
1420      }
1421#line 2150
1422      return (retValue_acc);
1423    } else {
1424#line 2142 "Elevator.c"
1425      retValue_acc = 0;
1426#line 2144
1427      return (retValue_acc);
1428    }
1429  } else {
1430    {
1431#line 2148 "Elevator.c"
1432    retValue_acc = stopRequestedAtCurrentFloor__wrappee__empty();
1433    }
1434#line 2150
1435    return (retValue_acc);
1436  }
1437#line 2157 "Elevator.c"
1438  return (retValue_acc);
1439}
1440}
1441#line 310 "Elevator.c"
1442int getReverseHeading(int ofHeading ) 
1443{ int retValue_acc ;
1444
1445  {
1446#line 313 "Elevator.c"
1447  if (ofHeading == 0) {
1448#line 2182
1449    retValue_acc = 1;
1450#line 2184
1451    return (retValue_acc);
1452  } else {
1453#line 2188 "Elevator.c"
1454    retValue_acc = 0;
1455#line 2190
1456    return (retValue_acc);
1457  }
1458#line 2197 "Elevator.c"
1459  return (retValue_acc);
1460}
1461}
1462#line 317 "Elevator.c"
1463void processWaitingOnFloor(int floorID ) 
1464{ int tmp ;
1465  int tmp___0 ;
1466  int tmp___1 ;
1467  int tmp___2 ;
1468  int tmp___3 ;
1469  int tmp___4 ;
1470  int tmp___5 ;
1471  int tmp___6 ;
1472  int tmp___7 ;
1473  int tmp___8 ;
1474  int tmp___9 ;
1475  int tmp___10 ;
1476
1477  {
1478  {
1479#line 323
1480  tmp___0 = isPersonOnFloor(0, floorID);
1481  }
1482#line 323
1483  if (tmp___0) {
1484    {
1485#line 319
1486    removePersonFromFloor(0, floorID);
1487#line 320
1488    tmp = getDestination(0);
1489#line 320
1490    pressInLiftFloorButton(tmp);
1491#line 321
1492    enterElevator(0);
1493    }
1494  } else {
1495
1496  }
1497  {
1498#line 323
1499  tmp___2 = isPersonOnFloor(1, floorID);
1500  }
1501#line 323
1502  if (tmp___2) {
1503    {
1504#line 324
1505    removePersonFromFloor(1, floorID);
1506#line 325
1507    tmp___1 = getDestination(1);
1508#line 325
1509    pressInLiftFloorButton(tmp___1);
1510#line 326
1511    enterElevator(1);
1512    }
1513  } else {
1514
1515  }
1516  {
1517#line 328
1518  tmp___4 = isPersonOnFloor(2, floorID);
1519  }
1520#line 328
1521  if (tmp___4) {
1522    {
1523#line 329
1524    removePersonFromFloor(2, floorID);
1525#line 330
1526    tmp___3 = getDestination(2);
1527#line 330
1528    pressInLiftFloorButton(tmp___3);
1529#line 331
1530    enterElevator(2);
1531    }
1532  } else {
1533
1534  }
1535  {
1536#line 333
1537  tmp___6 = isPersonOnFloor(3, floorID);
1538  }
1539#line 333
1540  if (tmp___6) {
1541    {
1542#line 334
1543    removePersonFromFloor(3, floorID);
1544#line 335
1545    tmp___5 = getDestination(3);
1546#line 335
1547    pressInLiftFloorButton(tmp___5);
1548#line 336
1549    enterElevator(3);
1550    }
1551  } else {
1552
1553  }
1554  {
1555#line 338
1556  tmp___8 = isPersonOnFloor(4, floorID);
1557  }
1558#line 338
1559  if (tmp___8) {
1560    {
1561#line 339
1562    removePersonFromFloor(4, floorID);
1563#line 340
1564    tmp___7 = getDestination(4);
1565#line 340
1566    pressInLiftFloorButton(tmp___7);
1567#line 341
1568    enterElevator(4);
1569    }
1570  } else {
1571
1572  }
1573  {
1574#line 343
1575  tmp___10 = isPersonOnFloor(5, floorID);
1576  }
1577#line 343
1578  if (tmp___10) {
1579    {
1580#line 344
1581    removePersonFromFloor(5, floorID);
1582#line 345
1583    tmp___9 = getDestination(5);
1584#line 345
1585    pressInLiftFloorButton(tmp___9);
1586#line 346
1587    enterElevator(5);
1588    }
1589  } else {
1590
1591  }
1592  {
1593#line 348
1594  resetCallOnFloor(floorID);
1595  }
1596#line 2275 "Elevator.c"
1597  return;
1598}
1599}
1600#line 2277
1601void __utac_acc__Specification3_spec__1(void) ;
1602#line 2280
1603void __utac_acc__Specification3_spec__2(void) ;
1604#line 352 "Elevator.c"
1605void timeShift(void) 
1606{ int tmp ;
1607  int tmp___0 ;
1608  int tmp___1 ;
1609  int tmp___2 ;
1610  int tmp___3 ;
1611  int tmp___4 ;
1612  int tmp___5 ;
1613  int tmp___6 ;
1614  int tmp___7 ;
1615  int tmp___8 ;
1616  int tmp___9 ;
1617
1618  {
1619  {
1620#line 2291 "Elevator.c"
1621  __utac_acc__Specification3_spec__1();
1622#line 385 "Elevator.c"
1623  tmp___9 = stopRequestedAtCurrentFloor();
1624  }
1625#line 385
1626  if (tmp___9) {
1627#line 357
1628    doorState = 1;
1629#line 359
1630    if (persons_0) {
1631      {
1632#line 359
1633      tmp = getDestination(0);
1634      }
1635#line 359
1636      if (tmp == currentFloorID) {
1637        {
1638#line 360
1639        leaveElevator(0);
1640        }
1641      } else {
1642
1643      }
1644    } else {
1645
1646    }
1647#line 360
1648    if (persons_1) {
1649      {
1650#line 360
1651      tmp___0 = getDestination(1);
1652      }
1653#line 360
1654      if (tmp___0 == currentFloorID) {
1655        {
1656#line 361
1657        leaveElevator(1);
1658        }
1659      } else {
1660
1661      }
1662    } else {
1663
1664    }
1665#line 361
1666    if (persons_2) {
1667      {
1668#line 361
1669      tmp___1 = getDestination(2);
1670      }
1671#line 361
1672      if (tmp___1 == currentFloorID) {
1673        {
1674#line 362
1675        leaveElevator(2);
1676        }
1677      } else {
1678
1679      }
1680    } else {
1681
1682    }
1683#line 362
1684    if (persons_3) {
1685      {
1686#line 362
1687      tmp___2 = getDestination(3);
1688      }
1689#line 362
1690      if (tmp___2 == currentFloorID) {
1691        {
1692#line 363
1693        leaveElevator(3);
1694        }
1695      } else {
1696
1697      }
1698    } else {
1699
1700    }
1701#line 363
1702    if (persons_4) {
1703      {
1704#line 363
1705      tmp___3 = getDestination(4);
1706      }
1707#line 363
1708      if (tmp___3 == currentFloorID) {
1709        {
1710#line 364
1711        leaveElevator(4);
1712        }
1713      } else {
1714
1715      }
1716    } else {
1717
1718    }
1719#line 364
1720    if (persons_5) {
1721      {
1722#line 364
1723      tmp___4 = getDestination(5);
1724      }
1725#line 364
1726      if (tmp___4 == currentFloorID) {
1727        {
1728#line 365
1729        leaveElevator(5);
1730        }
1731      } else {
1732
1733      }
1734    } else {
1735
1736    }
1737    {
1738#line 365
1739    processWaitingOnFloor(currentFloorID);
1740#line 366
1741    resetFloorButton(currentFloorID);
1742    }
1743  } else {
1744#line 372
1745    if (doorState == 1) {
1746#line 369
1747      doorState = 0;
1748    } else {
1749
1750    }
1751    {
1752#line 372
1753    tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
1754    }
1755#line 372
1756    if (tmp___8) {
1757      {
1758#line 375
1759      continueInDirection(currentHeading);
1760      }
1761    } else {
1762      {
1763#line 376
1764      tmp___6 = getReverseHeading(currentHeading);
1765#line 376
1766      tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
1767      }
1768#line 376
1769      if (tmp___7) {
1770        {
1771#line 379
1772        tmp___5 = getReverseHeading(currentHeading);
1773#line 379
1774        continueInDirection(tmp___5);
1775        }
1776      } else {
1777        {
1778#line 383
1779        continueInDirection(currentHeading);
1780        }
1781      }
1782    }
1783  }
1784  {
1785#line 2348 "Elevator.c"
1786  __utac_acc__Specification3_spec__2();
1787  }
1788#line 2354
1789  return;
1790}
1791}
1792#line 388 "Elevator.c"
1793void printState(void) 
1794{ int tmp ;
1795  int tmp___0 ;
1796  int tmp___1 ;
1797  int tmp___2 ;
1798  int tmp___3 ;
1799  char const   * __restrict  __cil_tmp6 ;
1800  char const   * __restrict  __cil_tmp7 ;
1801  char const   * __restrict  __cil_tmp8 ;
1802  char const   * __restrict  __cil_tmp9 ;
1803  char const   * __restrict  __cil_tmp10 ;
1804  char const   * __restrict  __cil_tmp11 ;
1805  char const   * __restrict  __cil_tmp12 ;
1806  char const   * __restrict  __cil_tmp13 ;
1807  char const   * __restrict  __cil_tmp14 ;
1808  char const   * __restrict  __cil_tmp15 ;
1809  char const   * __restrict  __cil_tmp16 ;
1810  char const   * __restrict  __cil_tmp17 ;
1811  char const   * __restrict  __cil_tmp18 ;
1812  char const   * __restrict  __cil_tmp19 ;
1813  char const   * __restrict  __cil_tmp20 ;
1814  char const   * __restrict  __cil_tmp21 ;
1815  char const   * __restrict  __cil_tmp22 ;
1816  char const   * __restrict  __cil_tmp23 ;
1817  char const   * __restrict  __cil_tmp24 ;
1818  char const   * __restrict  __cil_tmp25 ;
1819  char const   * __restrict  __cil_tmp26 ;
1820
1821  {
1822  {
1823#line 389
1824  __cil_tmp6 = (char const   * __restrict  )"Elevator ";
1825#line 389
1826  printf(__cil_tmp6);
1827  }
1828#line 390
1829  if (doorState) {
1830    {
1831#line 391
1832    __cil_tmp7 = (char const   * __restrict  )"[_]";
1833#line 391
1834    printf(__cil_tmp7);
1835    }
1836  } else {
1837    {
1838#line 392
1839    __cil_tmp8 = (char const   * __restrict  )"[] ";
1840#line 392
1841    printf(__cil_tmp8);
1842    }
1843  }
1844  {
1845#line 392
1846  __cil_tmp9 = (char const   * __restrict  )" at ";
1847#line 392
1848  printf(__cil_tmp9);
1849#line 393
1850  __cil_tmp10 = (char const   * __restrict  )"%i";
1851#line 393
1852  printf(__cil_tmp10, currentFloorID);
1853#line 394
1854  __cil_tmp11 = (char const   * __restrict  )" heading ";
1855#line 394
1856  printf(__cil_tmp11);
1857  }
1858#line 395
1859  if (currentHeading) {
1860    {
1861#line 396
1862    __cil_tmp12 = (char const   * __restrict  )"up";
1863#line 396
1864    printf(__cil_tmp12);
1865    }
1866  } else {
1867    {
1868#line 397
1869    __cil_tmp13 = (char const   * __restrict  )"down";
1870#line 397
1871    printf(__cil_tmp13);
1872    }
1873  }
1874  {
1875#line 397
1876  __cil_tmp14 = (char const   * __restrict  )" IL_p:";
1877#line 397
1878  printf(__cil_tmp14);
1879  }
1880#line 398
1881  if (floorButtons_0) {
1882    {
1883#line 399
1884    __cil_tmp15 = (char const   * __restrict  )" %i";
1885#line 399
1886    printf(__cil_tmp15, 0);
1887    }
1888  } else {
1889
1890  }
1891#line 399
1892  if (floorButtons_1) {
1893    {
1894#line 400
1895    __cil_tmp16 = (char const   * __restrict  )" %i";
1896#line 400
1897    printf(__cil_tmp16, 1);
1898    }
1899  } else {
1900
1901  }
1902#line 400
1903  if (floorButtons_2) {
1904    {
1905#line 401
1906    __cil_tmp17 = (char const   * __restrict  )" %i";
1907#line 401
1908    printf(__cil_tmp17, 2);
1909    }
1910  } else {
1911
1912  }
1913#line 401
1914  if (floorButtons_3) {
1915    {
1916#line 402
1917    __cil_tmp18 = (char const   * __restrict  )" %i";
1918#line 402
1919    printf(__cil_tmp18, 3);
1920    }
1921  } else {
1922
1923  }
1924#line 402
1925  if (floorButtons_4) {
1926    {
1927#line 403
1928    __cil_tmp19 = (char const   * __restrict  )" %i";
1929#line 403
1930    printf(__cil_tmp19, 4);
1931    }
1932  } else {
1933
1934  }
1935  {
1936#line 403
1937  __cil_tmp20 = (char const   * __restrict  )" F_p:";
1938#line 403
1939  printf(__cil_tmp20);
1940#line 404
1941  tmp = isFloorCalling(0);
1942  }
1943#line 404
1944  if (tmp) {
1945    {
1946#line 405
1947    __cil_tmp21 = (char const   * __restrict  )" %i";
1948#line 405
1949    printf(__cil_tmp21, 0);
1950    }
1951  } else {
1952
1953  }
1954  {
1955#line 405
1956  tmp___0 = isFloorCalling(1);
1957  }
1958#line 405
1959  if (tmp___0) {
1960    {
1961#line 406
1962    __cil_tmp22 = (char const   * __restrict  )" %i";
1963#line 406
1964    printf(__cil_tmp22, 1);
1965    }
1966  } else {
1967
1968  }
1969  {
1970#line 406
1971  tmp___1 = isFloorCalling(2);
1972  }
1973#line 406
1974  if (tmp___1) {
1975    {
1976#line 407
1977    __cil_tmp23 = (char const   * __restrict  )" %i";
1978#line 407
1979    printf(__cil_tmp23, 2);
1980    }
1981  } else {
1982
1983  }
1984  {
1985#line 407
1986  tmp___2 = isFloorCalling(3);
1987  }
1988#line 407
1989  if (tmp___2) {
1990    {
1991#line 408
1992    __cil_tmp24 = (char const   * __restrict  )" %i";
1993#line 408
1994    printf(__cil_tmp24, 3);
1995    }
1996  } else {
1997
1998  }
1999  {
2000#line 408
2001  tmp___3 = isFloorCalling(4);
2002  }
2003#line 408
2004  if (tmp___3) {
2005    {
2006#line 409
2007    __cil_tmp25 = (char const   * __restrict  )" %i";
2008#line 409
2009    printf(__cil_tmp25, 4);
2010    }
2011  } else {
2012
2013  }
2014  {
2015#line 409
2016  __cil_tmp26 = (char const   * __restrict  )"\n";
2017#line 409
2018  printf(__cil_tmp26);
2019  }
2020#line 2424 "Elevator.c"
2021  return;
2022}
2023}
2024#line 413 "Elevator.c"
2025int existInLiftCallsInDirection(int d ) 
2026{ int retValue_acc ;
2027  int i ;
2028  int i___0 ;
2029
2030  {
2031#line 434
2032  if (d == 1) {
2033#line 415 "Elevator.c"
2034    i = 0;
2035#line 416
2036    i = currentFloorID + 1;
2037    {
2038#line 416
2039    while (1) {
2040      while_0_continue: /* CIL Label */ ;
2041#line 416
2042      if (i < 5) {
2043
2044      } else {
2045        goto while_0_break;
2046      }
2047#line 422
2048      if (i == 0) {
2049#line 422 "Elevator.c"
2050        if (floorButtons_0) {
2051#line 2452
2052          retValue_acc = 1;
2053#line 2454
2054          return (retValue_acc);
2055        } else {
2056          goto _L___2;
2057        }
2058      } else {
2059        _L___2: /* CIL Label */ 
2060#line 2456
2061        if (i == 1) {
2062#line 2456
2063          if (floorButtons_1) {
2064#line 2459
2065            retValue_acc = 1;
2066#line 2461
2067            return (retValue_acc);
2068          } else {
2069            goto _L___1;
2070          }
2071        } else {
2072          _L___1: /* CIL Label */ 
2073#line 2463
2074          if (i == 2) {
2075#line 2463
2076            if (floorButtons_2) {
2077#line 2466
2078              retValue_acc = 1;
2079#line 2468
2080              return (retValue_acc);
2081            } else {
2082              goto _L___0;
2083            }
2084          } else {
2085            _L___0: /* CIL Label */ 
2086#line 2470
2087            if (i == 3) {
2088#line 2470
2089              if (floorButtons_3) {
2090#line 2473
2091                retValue_acc = 1;
2092#line 2475
2093                return (retValue_acc);
2094              } else {
2095                goto _L;
2096              }
2097            } else {
2098              _L: /* CIL Label */ 
2099#line 2477
2100              if (i == 4) {
2101#line 2477
2102                if (floorButtons_4) {
2103#line 2480 "Elevator.c"
2104                  retValue_acc = 1;
2105#line 2482
2106                  return (retValue_acc);
2107                } else {
2108
2109                }
2110              } else {
2111
2112              }
2113            }
2114          }
2115        }
2116      }
2117#line 416
2118      i = i + 1;
2119    }
2120    while_0_break: /* CIL Label */ ;
2121    }
2122  } else {
2123#line 2484 "Elevator.c"
2124    if (d == 0) {
2125#line 424
2126      i___0 = 0;
2127#line 425
2128      i___0 = currentFloorID - 1;
2129      {
2130#line 425
2131      while (1) {
2132        while_1_continue: /* CIL Label */ ;
2133#line 425
2134        if (i___0 >= 0) {
2135
2136        } else {
2137          goto while_1_break;
2138        }
2139#line 425
2140        i___0 = currentFloorID + 1;
2141        {
2142#line 425
2143        while (1) {
2144          while_2_continue: /* CIL Label */ ;
2145#line 425
2146          if (i___0 < 5) {
2147
2148          } else {
2149            goto while_2_break;
2150          }
2151#line 432
2152          if (i___0 == 0) {
2153#line 432 "Elevator.c"
2154            if (floorButtons_0) {
2155#line 2496
2156              retValue_acc = 1;
2157#line 2498
2158              return (retValue_acc);
2159            } else {
2160              goto _L___6;
2161            }
2162          } else {
2163            _L___6: /* CIL Label */ 
2164#line 2500
2165            if (i___0 == 1) {
2166#line 2500
2167              if (floorButtons_1) {
2168#line 2503
2169                retValue_acc = 1;
2170#line 2505
2171                return (retValue_acc);
2172              } else {
2173                goto _L___5;
2174              }
2175            } else {
2176              _L___5: /* CIL Label */ 
2177#line 2507
2178              if (i___0 == 2) {
2179#line 2507
2180                if (floorButtons_2) {
2181#line 2510
2182                  retValue_acc = 1;
2183#line 2512
2184                  return (retValue_acc);
2185                } else {
2186                  goto _L___4;
2187                }
2188              } else {
2189                _L___4: /* CIL Label */ 
2190#line 2514
2191                if (i___0 == 3) {
2192#line 2514
2193                  if (floorButtons_3) {
2194#line 2517
2195                    retValue_acc = 1;
2196#line 2519
2197                    return (retValue_acc);
2198                  } else {
2199                    goto _L___3;
2200                  }
2201                } else {
2202                  _L___3: /* CIL Label */ 
2203#line 2521
2204                  if (i___0 == 4) {
2205#line 2521
2206                    if (floorButtons_4) {
2207#line 2524 "Elevator.c"
2208                      retValue_acc = 1;
2209#line 2526
2210                      return (retValue_acc);
2211                    } else {
2212
2213                    }
2214                  } else {
2215
2216                  }
2217                }
2218              }
2219            }
2220          }
2221#line 425
2222          i___0 = i___0 + 1;
2223        }
2224        while_2_break: /* CIL Label */ ;
2225        }
2226#line 425
2227        i___0 = i___0 - 1;
2228      }
2229      while_1_break: /* CIL Label */ ;
2230      }
2231    } else {
2232
2233    }
2234  }
2235#line 2531 "Elevator.c"
2236  retValue_acc = 0;
2237#line 2533
2238  return (retValue_acc);
2239#line 2540
2240  return (retValue_acc);
2241}
2242}
2243#line 436 "Elevator.c"
2244int isExecutiveFloorCalling(void) 
2245{ int retValue_acc ;
2246
2247  {
2248  {
2249#line 2562 "Elevator.c"
2250  retValue_acc = isFloorCalling(executiveFloor);
2251  }
2252#line 2564
2253  return (retValue_acc);
2254#line 2571
2255  return (retValue_acc);
2256}
2257}
2258#line 440 "Elevator.c"
2259int isExecutiveFloor(int floorID ) 
2260{ int retValue_acc ;
2261
2262  {
2263#line 2593 "Elevator.c"
2264  retValue_acc = executiveFloor == floorID;
2265#line 2595
2266  return (retValue_acc);
2267#line 2602
2268  return (retValue_acc);
2269}
2270}
2271#line 1 "UnitTests.o"
2272#pragma merger(0,"UnitTests.i","")
2273#line 12 "Person.h"
2274int getOrigin(int person ) ;
2275#line 20 "Floor.h"
2276void initPersonOnFloor(int person , int floor ) ;
2277#line 13 "UnitTests.c"
2278int cleanupTimeShifts  =    12;
2279#line 24 "UnitTests.c"
2280void spec1(void) 
2281{ int tmp ;
2282  int tmp___0 ;
2283  int i ;
2284  int tmp___1 ;
2285
2286  {
2287  {
2288#line 25
2289  initBottomUp();
2290#line 26
2291  tmp = getOrigin(5);
2292#line 26
2293  initPersonOnFloor(5, tmp);
2294#line 27
2295  printState();
2296#line 30
2297  tmp___0 = getOrigin(2);
2298#line 30
2299  initPersonOnFloor(2, tmp___0);
2300#line 31
2301  printState();
2302#line 35
2303  i = 0;
2304  }
2305  {
2306#line 35
2307  while (1) {
2308    while_3_continue: /* CIL Label */ ;
2309#line 35
2310    if (i < cleanupTimeShifts) {
2311      {
2312#line 35
2313      tmp___1 = isBlocked();
2314      }
2315#line 35
2316      if (tmp___1 != 1) {
2317
2318      } else {
2319        goto while_3_break;
2320      }
2321    } else {
2322      goto while_3_break;
2323    }
2324    {
2325#line 36
2326    timeShift();
2327#line 37
2328    printState();
2329#line 35
2330    i = i + 1;
2331    }
2332  }
2333  while_3_break: /* CIL Label */ ;
2334  }
2335#line 1077 "UnitTests.c"
2336  return;
2337}
2338}
2339#line 42 "UnitTests.c"
2340void spec14(void) 
2341{ int tmp ;
2342  int tmp___0 ;
2343  int i ;
2344  int tmp___1 ;
2345
2346  {
2347  {
2348#line 43
2349  initTopDown();
2350#line 44
2351  tmp = getOrigin(5);
2352#line 44
2353  initPersonOnFloor(5, tmp);
2354#line 45
2355  printState();
2356#line 47
2357  timeShift();
2358#line 48
2359  timeShift();
2360#line 49
2361  timeShift();
2362#line 50
2363  timeShift();
2364#line 52
2365  tmp___0 = getOrigin(0);
2366#line 52
2367  initPersonOnFloor(0, tmp___0);
2368#line 53
2369  printState();
2370#line 57
2371  i = 0;
2372  }
2373  {
2374#line 57
2375  while (1) {
2376    while_4_continue: /* CIL Label */ ;
2377#line 57
2378    if (i < cleanupTimeShifts) {
2379      {
2380#line 57
2381      tmp___1 = isBlocked();
2382      }
2383#line 57
2384      if (tmp___1 != 1) {
2385
2386      } else {
2387        goto while_4_break;
2388      }
2389    } else {
2390      goto while_4_break;
2391    }
2392    {
2393#line 58
2394    timeShift();
2395#line 59
2396    printState();
2397#line 57
2398    i = i + 1;
2399    }
2400  }
2401  while_4_break: /* CIL Label */ ;
2402  }
2403#line 1123 "UnitTests.c"
2404  return;
2405}
2406}
2407#line 1 "Person.o"
2408#pragma merger(0,"Person.i","")
2409#line 20 "Person.c"
2410int getWeight(int person ) 
2411{ int retValue_acc ;
2412
2413  {
2414#line 35 "Person.c"
2415  if (person == 0) {
2416#line 974
2417    retValue_acc = 40;
2418#line 976
2419    return (retValue_acc);
2420  } else {
2421#line 978
2422    if (person == 1) {
2423#line 983
2424      retValue_acc = 40;
2425#line 985
2426      return (retValue_acc);
2427    } else {
2428#line 987
2429      if (person == 2) {
2430#line 992
2431        retValue_acc = 40;
2432#line 994
2433        return (retValue_acc);
2434      } else {
2435#line 996
2436        if (person == 3) {
2437#line 1001
2438          retValue_acc = 40;
2439#line 1003
2440          return (retValue_acc);
2441        } else {
2442#line 1005
2443          if (person == 4) {
2444#line 1010
2445            retValue_acc = 30;
2446#line 1012
2447            return (retValue_acc);
2448          } else {
2449#line 1014
2450            if (person == 5) {
2451#line 1019
2452              retValue_acc = 150;
2453#line 1021
2454              return (retValue_acc);
2455            } else {
2456#line 1027 "Person.c"
2457              retValue_acc = 0;
2458#line 1029
2459              return (retValue_acc);
2460            }
2461          }
2462        }
2463      }
2464    }
2465  }
2466#line 1036 "Person.c"
2467  return (retValue_acc);
2468}
2469}
2470#line 39 "Person.c"
2471int getOrigin(int person ) 
2472{ int retValue_acc ;
2473
2474  {
2475#line 54 "Person.c"
2476  if (person == 0) {
2477#line 1061
2478    retValue_acc = 4;
2479#line 1063
2480    return (retValue_acc);
2481  } else {
2482#line 1065
2483    if (person == 1) {
2484#line 1070
2485      retValue_acc = 3;
2486#line 1072
2487      return (retValue_acc);
2488    } else {
2489#line 1074
2490      if (person == 2) {
2491#line 1079
2492        retValue_acc = 2;
2493#line 1081
2494        return (retValue_acc);
2495      } else {
2496#line 1083
2497        if (person == 3) {
2498#line 1088
2499          retValue_acc = 1;
2500#line 1090
2501          return (retValue_acc);
2502        } else {
2503#line 1092
2504          if (person == 4) {
2505#line 1097
2506            retValue_acc = 0;
2507#line 1099
2508            return (retValue_acc);
2509          } else {
2510#line 1101
2511            if (person == 5) {
2512#line 1106
2513              retValue_acc = 1;
2514#line 1108
2515              return (retValue_acc);
2516            } else {
2517#line 1114 "Person.c"
2518              retValue_acc = 0;
2519#line 1116
2520              return (retValue_acc);
2521            }
2522          }
2523        }
2524      }
2525    }
2526  }
2527#line 1123 "Person.c"
2528  return (retValue_acc);
2529}
2530}
2531#line 57 "Person.c"
2532int getDestination(int person ) 
2533{ int retValue_acc ;
2534
2535  {
2536#line 72 "Person.c"
2537  if (person == 0) {
2538#line 1148
2539    retValue_acc = 0;
2540#line 1150
2541    return (retValue_acc);
2542  } else {
2543#line 1152
2544    if (person == 1) {
2545#line 1157
2546      retValue_acc = 0;
2547#line 1159
2548      return (retValue_acc);
2549    } else {
2550#line 1161
2551      if (person == 2) {
2552#line 1166
2553        retValue_acc = 1;
2554#line 1168
2555        return (retValue_acc);
2556      } else {
2557#line 1170
2558        if (person == 3) {
2559#line 1175
2560          retValue_acc = 3;
2561#line 1177
2562          return (retValue_acc);
2563        } else {
2564#line 1179
2565          if (person == 4) {
2566#line 1184
2567            retValue_acc = 1;
2568#line 1186
2569            return (retValue_acc);
2570          } else {
2571#line 1188
2572            if (person == 5) {
2573#line 1193
2574              retValue_acc = 3;
2575#line 1195
2576              return (retValue_acc);
2577            } else {
2578#line 1201 "Person.c"
2579              retValue_acc = 0;
2580#line 1203
2581              return (retValue_acc);
2582            }
2583          }
2584        }
2585      }
2586    }
2587  }
2588#line 1210 "Person.c"
2589  return (retValue_acc);
2590}
2591}
2592#line 1 "Specification3_spec.o"
2593#pragma merger(0,"Specification3_spec.i","")
2594#line 4 "wsllib.h"
2595void __automaton_fail(void) ;
2596#line 7 "Specification3_spec.c"
2597int expectedDirection  =    0;
2598#line 11 "Specification3_spec.c"
2599void __utac_acc__Specification3_spec__1(void) 
2600{ int currentFloorID___0 ;
2601  int tmp ;
2602  int tmp___0 ;
2603  int tmp___1 ;
2604  int tmp___2 ;
2605  int tmp___3 ;
2606  int tmp___4 ;
2607  int tmp___5 ;
2608  int tmp___6 ;
2609  int tmp___7 ;
2610  int tmp___8 ;
2611  int tmp___9 ;
2612  int tmp___10 ;
2613
2614  {
2615  {
2616#line 13
2617  expectedDirection = 0;
2618#line 14
2619  tmp = getCurrentFloorID();
2620#line 14
2621  currentFloorID___0 = tmp;
2622#line 15
2623  tmp___10 = getCurrentHeading();
2624  }
2625#line 15
2626  if (tmp___10 == 1) {
2627#line 21
2628    if (currentFloorID___0 < 0) {
2629      {
2630#line 21
2631      tmp___4 = buttonForFloorIsPressed(0);
2632      }
2633#line 21
2634      if (tmp___4) {
2635#line 22
2636        expectedDirection = 1;
2637      } else {
2638        goto _L___2;
2639      }
2640    } else {
2641      _L___2: /* CIL Label */ 
2642#line 23
2643      if (currentFloorID___0 < 1) {
2644        {
2645#line 23
2646        tmp___3 = buttonForFloorIsPressed(1);
2647        }
2648#line 23
2649        if (tmp___3) {
2650#line 24
2651          expectedDirection = 1;
2652        } else {
2653          goto _L___1;
2654        }
2655      } else {
2656        _L___1: /* CIL Label */ 
2657#line 25
2658        if (currentFloorID___0 < 2) {
2659          {
2660#line 25
2661          tmp___2 = buttonForFloorIsPressed(2);
2662          }
2663#line 25
2664          if (tmp___2) {
2665#line 26
2666            expectedDirection = 1;
2667          } else {
2668            goto _L___0;
2669          }
2670        } else {
2671          _L___0: /* CIL Label */ 
2672#line 27
2673          if (currentFloorID___0 < 3) {
2674            {
2675#line 27
2676            tmp___1 = buttonForFloorIsPressed(3);
2677            }
2678#line 27
2679            if (tmp___1) {
2680#line 28
2681              expectedDirection = 1;
2682            } else {
2683              goto _L;
2684            }
2685          } else {
2686            _L: /* CIL Label */ 
2687#line 29
2688            if (currentFloorID___0 < 4) {
2689              {
2690#line 29
2691              tmp___0 = buttonForFloorIsPressed(4);
2692              }
2693#line 29
2694              if (tmp___0) {
2695#line 30
2696                expectedDirection = 1;
2697              } else {
2698
2699              }
2700            } else {
2701
2702            }
2703          }
2704        }
2705      }
2706    }
2707  } else {
2708#line 27
2709    if (currentFloorID___0 > 0) {
2710      {
2711#line 27
2712      tmp___9 = buttonForFloorIsPressed(0);
2713      }
2714#line 27
2715      if (tmp___9) {
2716#line 28
2717        expectedDirection = -1;
2718      } else {
2719        goto _L___6;
2720      }
2721    } else {
2722      _L___6: /* CIL Label */ 
2723#line 29
2724      if (currentFloorID___0 > 1) {
2725        {
2726#line 29
2727        tmp___8 = buttonForFloorIsPressed(1);
2728        }
2729#line 29
2730        if (tmp___8) {
2731#line 30
2732          expectedDirection = -1;
2733        } else {
2734          goto _L___5;
2735        }
2736      } else {
2737        _L___5: /* CIL Label */ 
2738#line 31
2739        if (currentFloorID___0 > 2) {
2740          {
2741#line 31
2742          tmp___7 = buttonForFloorIsPressed(2);
2743          }
2744#line 31
2745          if (tmp___7) {
2746#line 32
2747            expectedDirection = -1;
2748          } else {
2749            goto _L___4;
2750          }
2751        } else {
2752          _L___4: /* CIL Label */ 
2753#line 33
2754          if (currentFloorID___0 > 3) {
2755            {
2756#line 33
2757            tmp___6 = buttonForFloorIsPressed(3);
2758            }
2759#line 33
2760            if (tmp___6) {
2761#line 34
2762              expectedDirection = -1;
2763            } else {
2764              goto _L___3;
2765            }
2766          } else {
2767            _L___3: /* CIL Label */ 
2768#line 35
2769            if (currentFloorID___0 > 4) {
2770              {
2771#line 35
2772              tmp___5 = buttonForFloorIsPressed(4);
2773              }
2774#line 35
2775              if (tmp___5) {
2776#line 36
2777                expectedDirection = -1;
2778              } else {
2779
2780              }
2781            } else {
2782
2783            }
2784          }
2785        }
2786      }
2787    }
2788  }
2789#line 36
2790  return;
2791}
2792}
2793#line 31 "Specification3_spec.c"
2794void __utac_acc__Specification3_spec__2(void) 
2795{ int tmp ;
2796  int tmp___0 ;
2797
2798  {
2799#line 38
2800  if (expectedDirection == -1) {
2801    {
2802#line 38
2803    tmp___0 = getCurrentHeading();
2804    }
2805#line 38
2806    if (tmp___0 == 1) {
2807      {
2808#line 39
2809      __automaton_fail();
2810      }
2811    } else {
2812      goto _L;
2813    }
2814  } else {
2815    _L: /* CIL Label */ 
2816#line 40
2817    if (expectedDirection == 1) {
2818      {
2819#line 40
2820      tmp = getCurrentHeading();
2821      }
2822#line 40
2823      if (tmp == 0) {
2824        {
2825#line 41
2826        __automaton_fail();
2827        }
2828      } else {
2829
2830      }
2831    } else {
2832
2833    }
2834  }
2835#line 41
2836  return;
2837}
2838}
2839#line 1 "scenario.o"
2840#pragma merger(0,"scenario.i","")
2841#line 3 "scenario.c"
2842void bobCall(void) ;
2843#line 4
2844void threeTS(void) ;
2845#line 6
2846void cleanup(void) ;
2847#line 1 "scenario.c"
2848void test(void) 
2849{ 
2850
2851  {
2852  {
2853#line 2
2854  initTopDown();
2855#line 3
2856  bobCall();
2857#line 4
2858  threeTS();
2859#line 5
2860  bobCall();
2861#line 6
2862  cleanup();
2863  }
2864#line 59 "scenario.c"
2865  return;
2866}
2867}
2868#line 1 "Test.o"
2869#pragma merger(0,"Test.i","")
2870#line 544 "/usr/include/stdlib.h"
2871extern  __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
2872#line 17 "Test.c"
2873#line 23 "Test.c"
2874int get_nondetMinMax07(void) 
2875{ int retValue_acc ;
2876  int nd ;
2877  nd = __VERIFIER_nondet_int();
2878
2879  {
2880#line 26 "Test.c"
2881  if (nd == 0) {
2882#line 1108
2883    retValue_acc = 0;
2884#line 1110
2885    return (retValue_acc);
2886  } else {
2887#line 1112
2888    if (nd == 1) {
2889#line 1117
2890      retValue_acc = 1;
2891#line 1119
2892      return (retValue_acc);
2893    } else {
2894#line 1121
2895      if (nd == 2) {
2896#line 1126
2897        retValue_acc = 2;
2898#line 1128
2899        return (retValue_acc);
2900      } else {
2901#line 1130
2902        if (nd == 3) {
2903#line 1135
2904          retValue_acc = 3;
2905#line 1137
2906          return (retValue_acc);
2907        } else {
2908#line 1139
2909          if (nd == 4) {
2910#line 1144
2911            retValue_acc = 4;
2912#line 1146
2913            return (retValue_acc);
2914          } else {
2915#line 1148
2916            if (nd == 5) {
2917#line 1153
2918              retValue_acc = 5;
2919#line 1155
2920              return (retValue_acc);
2921            } else {
2922#line 1157
2923              if (nd == 6) {
2924#line 1162
2925                retValue_acc = 6;
2926#line 1164
2927                return (retValue_acc);
2928              } else {
2929#line 1166
2930                if (nd == 7) {
2931#line 1171 "Test.c"
2932                  retValue_acc = 7;
2933#line 1173
2934                  return (retValue_acc);
2935                } else {
2936                  {
2937#line 43
2938                  exit(0);
2939                  }
2940                }
2941              }
2942            }
2943          }
2944        }
2945      }
2946    }
2947  }
2948#line 1183 "Test.c"
2949  return (retValue_acc);
2950}
2951}
2952#line 48 "Test.c"
2953void bobCall(void) 
2954{ int tmp ;
2955
2956  {
2957  {
2958#line 48
2959  tmp = getOrigin(0);
2960#line 48
2961  initPersonOnFloor(0, tmp);
2962  }
2963#line 1207 "Test.c"
2964  return;
2965}
2966}
2967#line 50 "Test.c"
2968void aliceCall(void) 
2969{ int tmp ;
2970
2971  {
2972  {
2973#line 50
2974  tmp = getOrigin(1);
2975#line 50
2976  initPersonOnFloor(1, tmp);
2977  }
2978#line 1227 "Test.c"
2979  return;
2980}
2981}
2982#line 52 "Test.c"
2983void angelinaCall(void) 
2984{ int tmp ;
2985
2986  {
2987  {
2988#line 52
2989  tmp = getOrigin(2);
2990#line 52
2991  initPersonOnFloor(2, tmp);
2992  }
2993#line 1247 "Test.c"
2994  return;
2995}
2996}
2997#line 54 "Test.c"
2998void chuckCall(void) 
2999{ int tmp ;
3000
3001  {
3002  {
3003#line 54
3004  tmp = getOrigin(3);
3005#line 54
3006  initPersonOnFloor(3, tmp);
3007  }
3008#line 1267 "Test.c"
3009  return;
3010}
3011}
3012#line 56 "Test.c"
3013void monicaCall(void) 
3014{ int tmp ;
3015
3016  {
3017  {
3018#line 56
3019  tmp = getOrigin(4);
3020#line 56
3021  initPersonOnFloor(4, tmp);
3022  }
3023#line 1287 "Test.c"
3024  return;
3025}
3026}
3027#line 58 "Test.c"
3028void bigMacCall(void) 
3029{ int tmp ;
3030
3031  {
3032  {
3033#line 58
3034  tmp = getOrigin(5);
3035#line 58
3036  initPersonOnFloor(5, tmp);
3037  }
3038#line 1307 "Test.c"
3039  return;
3040}
3041}
3042#line 60 "Test.c"
3043void threeTS(void) 
3044{ 
3045
3046  {
3047  {
3048#line 60
3049  timeShift();
3050#line 60
3051  timeShift();
3052#line 60
3053  timeShift();
3054  }
3055#line 1331 "Test.c"
3056  return;
3057}
3058}
3059#line 62 "Test.c"
3060void cleanup(void) 
3061{ int i ;
3062  int tmp ;
3063  int tmp___0 ;
3064  int __cil_tmp4 ;
3065
3066  {
3067  {
3068#line 65
3069  timeShift();
3070#line 67
3071  i = 0;
3072  }
3073  {
3074#line 67
3075  while (1) {
3076    while_5_continue: /* CIL Label */ ;
3077    {
3078#line 67
3079    __cil_tmp4 = cleanupTimeShifts - 1;
3080#line 67
3081    if (i < __cil_tmp4) {
3082      {
3083#line 67
3084      tmp___0 = isBlocked();
3085      }
3086#line 67
3087      if (tmp___0 != 1) {
3088
3089      } else {
3090        goto while_5_break;
3091      }
3092    } else {
3093      goto while_5_break;
3094    }
3095    }
3096    {
3097#line 71
3098    tmp = isIdle();
3099    }
3100#line 71
3101    if (tmp) {
3102#line 72
3103      return;
3104    } else {
3105      {
3106#line 74
3107      timeShift();
3108      }
3109    }
3110#line 67
3111    i = i + 1;
3112  }
3113  while_5_break: /* CIL Label */ ;
3114  }
3115#line 1362 "Test.c"
3116  return;
3117}
3118}
3119#line 77 "Test.c"
3120void randomSequenceOfActions(void) 
3121{ int maxLength ;
3122  int tmp ;
3123  int counter ;
3124  int action ;
3125  int tmp___0 ;
3126  int origin ;
3127  int tmp___1 ;
3128  int tmp___2 ;
3129
3130  {
3131  {
3132#line 78
3133  maxLength = 4;
3134#line 79
3135  tmp = __VERIFIER_nondet_int();
3136  }
3137#line 79
3138  if (tmp) {
3139    {
3140#line 81
3141    initTopDown();
3142    }
3143  } else {
3144    {
3145#line 85
3146    initBottomUp();
3147    }
3148  }
3149#line 90
3150  counter = 0;
3151  {
3152#line 91
3153  while (1) {
3154    while_6_continue: /* CIL Label */ ;
3155#line 91
3156    if (counter < maxLength) {
3157
3158    } else {
3159      goto while_6_break;
3160    }
3161    {
3162#line 92
3163    counter = counter + 1;
3164#line 93
3165    tmp___0 = get_nondetMinMax07();
3166#line 93
3167    action = tmp___0;
3168    }
3169#line 99
3170    if (action < 6) {
3171      {
3172#line 100
3173      tmp___1 = getOrigin(action);
3174#line 100
3175      origin = tmp___1;
3176#line 101
3177      initPersonOnFloor(action, origin);
3178      }
3179    } else {
3180#line 102
3181      if (action == 6) {
3182        {
3183#line 103
3184        timeShift();
3185        }
3186      } else {
3187#line 104
3188        if (action == 7) {
3189          {
3190#line 106
3191          timeShift();
3192#line 107
3193          timeShift();
3194#line 108
3195          timeShift();
3196          }
3197        } else {
3198
3199        }
3200      }
3201    }
3202    {
3203#line 113
3204    tmp___2 = isBlocked();
3205    }
3206#line 113
3207    if (tmp___2) {
3208#line 114
3209      return;
3210    } else {
3211
3212    }
3213  }
3214  while_6_break: /* CIL Label */ ;
3215  }
3216  {
3217#line 117
3218  cleanup();
3219  }
3220#line 1433 "Test.c"
3221  return;
3222}
3223}
3224#line 122 "Test.c"
3225void runTest_Simple(void) 
3226{ 
3227
3228  {
3229  {
3230#line 123
3231  bigMacCall();
3232#line 124
3233  angelinaCall();
3234#line 125
3235  cleanup();
3236  }
3237#line 1457 "Test.c"
3238  return;
3239}
3240}
3241#line 130 "Test.c"
3242void Specification1(void) 
3243{ 
3244
3245  {
3246  {
3247#line 131
3248  bigMacCall();
3249#line 132
3250  angelinaCall();
3251#line 133
3252  cleanup();
3253  }
3254#line 1481 "Test.c"
3255  return;
3256}
3257}
3258#line 137 "Test.c"
3259void Specification2(void) 
3260{ 
3261
3262  {
3263  {
3264#line 138
3265  bigMacCall();
3266#line 139
3267  cleanup();
3268  }
3269#line 1503 "Test.c"
3270  return;
3271}
3272}
3273#line 142 "Test.c"
3274void Specification3(void) 
3275{ 
3276
3277  {
3278  {
3279#line 143
3280  bobCall();
3281#line 144
3282  timeShift();
3283#line 145
3284  timeShift();
3285#line 146
3286  timeShift();
3287#line 147
3288  timeShift();
3289#line 149
3290  timeShift();
3291#line 154
3292  bobCall();
3293#line 155
3294  cleanup();
3295  }
3296#line 1537 "Test.c"
3297  return;
3298}
3299}
3300#line 160 "Test.c"
3301void setup(void) 
3302{ 
3303
3304  {
3305#line 1555 "Test.c"
3306  return;
3307}
3308}
3309#line 165 "Test.c"
3310void runTest(void) 
3311{ 
3312
3313  {
3314  {
3315#line 168
3316  test();
3317  }
3318#line 1575 "Test.c"
3319  return;
3320}
3321}
3322#line 174 "Test.c"
3323void select_helpers(void) ;
3324#line 175
3325void select_features(void) ;
3326#line 176
3327int valid_product(void) ;
3328#line 173 "Test.c"
3329int main(void) 
3330{ int retValue_acc ;
3331  int tmp ;
3332
3333  {
3334  {
3335#line 174
3336  select_helpers();
3337#line 175
3338  select_features();
3339#line 176
3340  tmp = valid_product();
3341  }
3342#line 176
3343  if (tmp) {
3344    {
3345#line 177
3346    setup();
3347#line 178
3348    runTest();
3349    }
3350  } else {
3351
3352  }
3353#line 1604 "Test.c"
3354  retValue_acc = 0;
3355#line 1606
3356  return (retValue_acc);
3357#line 1613
3358  return (retValue_acc);
3359}
3360}
3361#line 1 "Floor.o"
3362#pragma merger(0,"Floor.i","")
3363#line 16 "Floor.h"
3364void callOnFloor(int floorID ) ;
3365#line 9 "Floor.c"
3366int calls_0  ;
3367#line 11 "Floor.c"
3368int calls_1  ;
3369#line 13 "Floor.c"
3370int calls_2  ;
3371#line 15 "Floor.c"
3372int calls_3  ;
3373#line 17 "Floor.c"
3374int calls_4  ;
3375#line 20 "Floor.c"
3376int personOnFloor_0_0  ;
3377#line 22 "Floor.c"
3378int personOnFloor_0_1  ;
3379#line 24 "Floor.c"
3380int personOnFloor_0_2  ;
3381#line 26 "Floor.c"
3382int personOnFloor_0_3  ;
3383#line 28 "Floor.c"
3384int personOnFloor_0_4  ;
3385#line 30 "Floor.c"
3386int personOnFloor_1_0  ;
3387#line 32 "Floor.c"
3388int personOnFloor_1_1  ;
3389#line 34 "Floor.c"
3390int personOnFloor_1_2  ;
3391#line 36 "Floor.c"
3392int personOnFloor_1_3  ;
3393#line 38 "Floor.c"
3394int personOnFloor_1_4  ;
3395#line 40 "Floor.c"
3396int personOnFloor_2_0  ;
3397#line 42 "Floor.c"
3398int personOnFloor_2_1  ;
3399#line 44 "Floor.c"
3400int personOnFloor_2_2  ;
3401#line 46 "Floor.c"
3402int personOnFloor_2_3  ;
3403#line 48 "Floor.c"
3404int personOnFloor_2_4  ;
3405#line 50 "Floor.c"
3406int personOnFloor_3_0  ;
3407#line 52 "Floor.c"
3408int personOnFloor_3_1  ;
3409#line 54 "Floor.c"
3410int personOnFloor_3_2  ;
3411#line 56 "Floor.c"
3412int personOnFloor_3_3  ;
3413#line 58 "Floor.c"
3414int personOnFloor_3_4  ;
3415#line 60 "Floor.c"
3416int personOnFloor_4_0  ;
3417#line 62 "Floor.c"
3418int personOnFloor_4_1  ;
3419#line 64 "Floor.c"
3420int personOnFloor_4_2  ;
3421#line 66 "Floor.c"
3422int personOnFloor_4_3  ;
3423#line 68 "Floor.c"
3424int personOnFloor_4_4  ;
3425#line 70 "Floor.c"
3426int personOnFloor_5_0  ;
3427#line 72 "Floor.c"
3428int personOnFloor_5_1  ;
3429#line 74 "Floor.c"
3430int personOnFloor_5_2  ;
3431#line 76 "Floor.c"
3432int personOnFloor_5_3  ;
3433#line 78 "Floor.c"
3434int personOnFloor_5_4  ;
3435#line 81 "Floor.c"
3436void initFloors(void) 
3437{ 
3438
3439  {
3440#line 82
3441  calls_0 = 0;
3442#line 83
3443  calls_1 = 0;
3444#line 84
3445  calls_2 = 0;
3446#line 85
3447  calls_3 = 0;
3448#line 86
3449  calls_4 = 0;
3450#line 87
3451  personOnFloor_0_0 = 0;
3452#line 88
3453  personOnFloor_0_1 = 0;
3454#line 89
3455  personOnFloor_0_2 = 0;
3456#line 90
3457  personOnFloor_0_3 = 0;
3458#line 91
3459  personOnFloor_0_4 = 0;
3460#line 92
3461  personOnFloor_1_0 = 0;
3462#line 93
3463  personOnFloor_1_1 = 0;
3464#line 94
3465  personOnFloor_1_2 = 0;
3466#line 95
3467  personOnFloor_1_3 = 0;
3468#line 96
3469  personOnFloor_1_4 = 0;
3470#line 97
3471  personOnFloor_2_0 = 0;
3472#line 98
3473  personOnFloor_2_1 = 0;
3474#line 99
3475  personOnFloor_2_2 = 0;
3476#line 100
3477  personOnFloor_2_3 = 0;
3478#line 101
3479  personOnFloor_2_4 = 0;
3480#line 102
3481  personOnFloor_3_0 = 0;
3482#line 103
3483  personOnFloor_3_1 = 0;
3484#line 104
3485  personOnFloor_3_2 = 0;
3486#line 105
3487  personOnFloor_3_3 = 0;
3488#line 106
3489  personOnFloor_3_4 = 0;
3490#line 107
3491  personOnFloor_4_0 = 0;
3492#line 108
3493  personOnFloor_4_1 = 0;
3494#line 109
3495  personOnFloor_4_2 = 0;
3496#line 110
3497  personOnFloor_4_3 = 0;
3498#line 111
3499  personOnFloor_4_4 = 0;
3500#line 112
3501  personOnFloor_5_0 = 0;
3502#line 113
3503  personOnFloor_5_1 = 0;
3504#line 114
3505  personOnFloor_5_2 = 0;
3506#line 115
3507  personOnFloor_5_3 = 0;
3508#line 116
3509  personOnFloor_5_4 = 0;
3510#line 1120 "Floor.c"
3511  return;
3512}
3513}
3514#line 120 "Floor.c"
3515int isFloorCalling(int floorID ) 
3516{ int retValue_acc ;
3517
3518  {
3519#line 126 "Floor.c"
3520  if (floorID == 0) {
3521#line 1139
3522    retValue_acc = calls_0;
3523#line 1141
3524    return (retValue_acc);
3525  } else {
3526#line 1143
3527    if (floorID == 1) {
3528#line 1146
3529      retValue_acc = calls_1;
3530#line 1148
3531      return (retValue_acc);
3532    } else {
3533#line 1150
3534      if (floorID == 2) {
3535#line 1153
3536        retValue_acc = calls_2;
3537#line 1155
3538        return (retValue_acc);
3539      } else {
3540#line 1157
3541        if (floorID == 3) {
3542#line 1160
3543          retValue_acc = calls_3;
3544#line 1162
3545          return (retValue_acc);
3546        } else {
3547#line 1164
3548          if (floorID == 4) {
3549#line 1167 "Floor.c"
3550            retValue_acc = calls_4;
3551#line 1169
3552            return (retValue_acc);
3553          } else {
3554
3555          }
3556        }
3557      }
3558    }
3559  }
3560#line 1174 "Floor.c"
3561  retValue_acc = 0;
3562#line 1176
3563  return (retValue_acc);
3564#line 1183
3565  return (retValue_acc);
3566}
3567}
3568#line 130 "Floor.c"
3569void resetCallOnFloor(int floorID ) 
3570{ 
3571
3572  {
3573#line 136
3574  if (floorID == 0) {
3575#line 137
3576    calls_0 = 0;
3577  } else {
3578#line 138
3579    if (floorID == 1) {
3580#line 139
3581      calls_1 = 0;
3582    } else {
3583#line 140
3584      if (floorID == 2) {
3585#line 141
3586        calls_2 = 0;
3587      } else {
3588#line 142
3589        if (floorID == 3) {
3590#line 143
3591          calls_3 = 0;
3592        } else {
3593#line 144
3594          if (floorID == 4) {
3595#line 145
3596            calls_4 = 0;
3597          } else {
3598
3599          }
3600        }
3601      }
3602    }
3603  }
3604#line 1216 "Floor.c"
3605  return;
3606}
3607}
3608#line 139 "Floor.c"
3609void callOnFloor(int floorID ) 
3610{ 
3611
3612  {
3613#line 145
3614  if (floorID == 0) {
3615#line 146
3616    calls_0 = 1;
3617  } else {
3618#line 147
3619    if (floorID == 1) {
3620#line 148
3621      calls_1 = 1;
3622    } else {
3623#line 149
3624      if (floorID == 2) {
3625#line 150
3626        calls_2 = 1;
3627      } else {
3628#line 151
3629        if (floorID == 3) {
3630#line 152
3631          calls_3 = 1;
3632        } else {
3633#line 153
3634          if (floorID == 4) {
3635#line 154
3636            calls_4 = 1;
3637          } else {
3638
3639          }
3640        }
3641      }
3642    }
3643  }
3644#line 1245 "Floor.c"
3645  return;
3646}
3647}
3648#line 148 "Floor.c"
3649int isPersonOnFloor(int person , int floor ) 
3650{ int retValue_acc ;
3651
3652  {
3653#line 185
3654  if (floor == 0) {
3655#line 156 "Floor.c"
3656    if (person == 0) {
3657#line 1267
3658      retValue_acc = personOnFloor_0_0;
3659#line 1269
3660      return (retValue_acc);
3661    } else {
3662#line 1271
3663      if (person == 1) {
3664#line 1274
3665        retValue_acc = personOnFloor_1_0;
3666#line 1276
3667        return (retValue_acc);
3668      } else {
3669#line 1278
3670        if (person == 2) {
3671#line 1281
3672          retValue_acc = personOnFloor_2_0;
3673#line 1283
3674          return (retValue_acc);
3675        } else {
3676#line 1285
3677          if (person == 3) {
3678#line 1288
3679            retValue_acc = personOnFloor_3_0;
3680#line 1290
3681            return (retValue_acc);
3682          } else {
3683#line 1292
3684            if (person == 4) {
3685#line 1295
3686              retValue_acc = personOnFloor_4_0;
3687#line 1297
3688              return (retValue_acc);
3689            } else {
3690#line 1299
3691              if (person == 5) {
3692#line 1302
3693                retValue_acc = personOnFloor_5_0;
3694#line 1304
3695                return (retValue_acc);
3696              } else {
3697
3698              }
3699            }
3700          }
3701        }
3702      }
3703    }
3704  } else {
3705#line 1306 "Floor.c"
3706    if (floor == 1) {
3707#line 163 "Floor.c"
3708      if (person == 0) {
3709#line 1312
3710        retValue_acc = personOnFloor_0_1;
3711#line 1314
3712        return (retValue_acc);
3713      } else {
3714#line 1316
3715        if (person == 1) {
3716#line 1319
3717          retValue_acc = personOnFloor_1_1;
3718#line 1321
3719          return (retValue_acc);
3720        } else {
3721#line 1323
3722          if (person == 2) {
3723#line 1326
3724            retValue_acc = personOnFloor_2_1;
3725#line 1328
3726            return (retValue_acc);
3727          } else {
3728#line 1330
3729            if (person == 3) {
3730#line 1333
3731              retValue_acc = personOnFloor_3_1;
3732#line 1335
3733              return (retValue_acc);
3734            } else {
3735#line 1337
3736              if (person == 4) {
3737#line 1340
3738                retValue_acc = personOnFloor_4_1;
3739#line 1342
3740                return (retValue_acc);
3741              } else {
3742#line 1344
3743                if (person == 5) {
3744#line 1347
3745                  retValue_acc = personOnFloor_5_1;
3746#line 1349
3747                  return (retValue_acc);
3748                } else {
3749
3750                }
3751              }
3752            }
3753          }
3754        }
3755      }
3756    } else {
3757#line 1351 "Floor.c"
3758      if (floor == 2) {
3759#line 170 "Floor.c"
3760        if (person == 0) {
3761#line 1357
3762          retValue_acc = personOnFloor_0_2;
3763#line 1359
3764          return (retValue_acc);
3765        } else {
3766#line 1361
3767          if (person == 1) {
3768#line 1364
3769            retValue_acc = personOnFloor_1_2;
3770#line 1366
3771            return (retValue_acc);
3772          } else {
3773#line 1368
3774            if (person == 2) {
3775#line 1371
3776              retValue_acc = personOnFloor_2_2;
3777#line 1373
3778              return (retValue_acc);
3779            } else {
3780#line 1375
3781              if (person == 3) {
3782#line 1378
3783                retValue_acc = personOnFloor_3_2;
3784#line 1380
3785                return (retValue_acc);
3786              } else {
3787#line 1382
3788                if (person == 4) {
3789#line 1385
3790                  retValue_acc = personOnFloor_4_2;
3791#line 1387
3792                  return (retValue_acc);
3793                } else {
3794#line 1389
3795                  if (person == 5) {
3796#line 1392
3797                    retValue_acc = personOnFloor_5_2;
3798#line 1394
3799                    return (retValue_acc);
3800                  } else {
3801
3802                  }
3803                }
3804              }
3805            }
3806          }
3807        }
3808      } else {
3809#line 1396 "Floor.c"
3810        if (floor == 3) {
3811#line 177 "Floor.c"
3812          if (person == 0) {
3813#line 1402
3814            retValue_acc = personOnFloor_0_3;
3815#line 1404
3816            return (retValue_acc);
3817          } else {
3818#line 1406
3819            if (person == 1) {
3820#line 1409
3821              retValue_acc = personOnFloor_1_3;
3822#line 1411
3823              return (retValue_acc);
3824            } else {
3825#line 1413
3826              if (person == 2) {
3827#line 1416
3828                retValue_acc = personOnFloor_2_3;
3829#line 1418
3830                return (retValue_acc);
3831              } else {
3832#line 1420
3833                if (person == 3) {
3834#line 1423
3835                  retValue_acc = personOnFloor_3_3;
3836#line 1425
3837                  return (retValue_acc);
3838                } else {
3839#line 1427
3840                  if (person == 4) {
3841#line 1430
3842                    retValue_acc = personOnFloor_4_3;
3843#line 1432
3844                    return (retValue_acc);
3845                  } else {
3846#line 1434
3847                    if (person == 5) {
3848#line 1437
3849                      retValue_acc = personOnFloor_5_3;
3850#line 1439
3851                      return (retValue_acc);
3852                    } else {
3853
3854                    }
3855                  }
3856                }
3857              }
3858            }
3859          }
3860        } else {
3861#line 1441 "Floor.c"
3862          if (floor == 4) {
3863#line 184 "Floor.c"
3864            if (person == 0) {
3865#line 1447
3866              retValue_acc = personOnFloor_0_4;
3867#line 1449
3868              return (retValue_acc);
3869            } else {
3870#line 1451
3871              if (person == 1) {
3872#line 1454
3873                retValue_acc = personOnFloor_1_4;
3874#line 1456
3875                return (retValue_acc);
3876              } else {
3877#line 1458
3878                if (person == 2) {
3879#line 1461
3880                  retValue_acc = personOnFloor_2_4;
3881#line 1463
3882                  return (retValue_acc);
3883                } else {
3884#line 1465
3885                  if (person == 3) {
3886#line 1468
3887                    retValue_acc = personOnFloor_3_4;
3888#line 1470
3889                    return (retValue_acc);
3890                  } else {
3891#line 1472
3892                    if (person == 4) {
3893#line 1475
3894                      retValue_acc = personOnFloor_4_4;
3895#line 1477
3896                      return (retValue_acc);
3897                    } else {
3898#line 1479
3899                      if (person == 5) {
3900#line 1482 "Floor.c"
3901                        retValue_acc = personOnFloor_5_4;
3902#line 1484
3903                        return (retValue_acc);
3904                      } else {
3905
3906                      }
3907                    }
3908                  }
3909                }
3910              }
3911            }
3912          } else {
3913
3914          }
3915        }
3916      }
3917    }
3918  }
3919#line 1489 "Floor.c"
3920  retValue_acc = 0;
3921#line 1491
3922  return (retValue_acc);
3923#line 1498
3924  return (retValue_acc);
3925}
3926}
3927#line 188 "Floor.c"
3928void initPersonOnFloor(int person , int floor ) 
3929{ 
3930
3931  {
3932#line 225
3933  if (floor == 0) {
3934#line 196
3935    if (person == 0) {
3936#line 197
3937      personOnFloor_0_0 = 1;
3938    } else {
3939#line 198
3940      if (person == 1) {
3941#line 199
3942        personOnFloor_1_0 = 1;
3943      } else {
3944#line 200
3945        if (person == 2) {
3946#line 201
3947          personOnFloor_2_0 = 1;
3948        } else {
3949#line 202
3950          if (person == 3) {
3951#line 203
3952            personOnFloor_3_0 = 1;
3953          } else {
3954#line 204
3955            if (person == 4) {
3956#line 205
3957              personOnFloor_4_0 = 1;
3958            } else {
3959#line 206
3960              if (person == 5) {
3961#line 207
3962                personOnFloor_5_0 = 1;
3963              } else {
3964
3965              }
3966            }
3967          }
3968        }
3969      }
3970    }
3971  } else {
3972#line 208
3973    if (floor == 1) {
3974#line 203
3975      if (person == 0) {
3976#line 204
3977        personOnFloor_0_1 = 1;
3978      } else {
3979#line 205
3980        if (person == 1) {
3981#line 206
3982          personOnFloor_1_1 = 1;
3983        } else {
3984#line 207
3985          if (person == 2) {
3986#line 208
3987            personOnFloor_2_1 = 1;
3988          } else {
3989#line 209
3990            if (person == 3) {
3991#line 210
3992              personOnFloor_3_1 = 1;
3993            } else {
3994#line 211
3995              if (person == 4) {
3996#line 212
3997                personOnFloor_4_1 = 1;
3998              } else {
3999#line 213
4000                if (person == 5) {
4001#line 214
4002                  personOnFloor_5_1 = 1;
4003                } else {
4004
4005                }
4006              }
4007            }
4008          }
4009        }
4010      }
4011    } else {
4012#line 215
4013      if (floor == 2) {
4014#line 210
4015        if (person == 0) {
4016#line 211
4017          personOnFloor_0_2 = 1;
4018        } else {
4019#line 212
4020          if (person == 1) {
4021#line 213
4022            personOnFloor_1_2 = 1;
4023          } else {
4024#line 214
4025            if (person == 2) {
4026#line 215
4027              personOnFloor_2_2 = 1;
4028            } else {
4029#line 216
4030              if (person == 3) {
4031#line 217
4032                personOnFloor_3_2 = 1;
4033              } else {
4034#line 218
4035                if (person == 4) {
4036#line 219
4037                  personOnFloor_4_2 = 1;
4038                } else {
4039#line 220
4040                  if (person == 5) {
4041#line 221
4042                    personOnFloor_5_2 = 1;
4043                  } else {
4044
4045                  }
4046                }
4047              }
4048            }
4049          }
4050        }
4051      } else {
4052#line 222
4053        if (floor == 3) {
4054#line 217
4055          if (person == 0) {
4056#line 218
4057            personOnFloor_0_3 = 1;
4058          } else {
4059#line 219
4060            if (person == 1) {
4061#line 220
4062              personOnFloor_1_3 = 1;
4063            } else {
4064#line 221
4065              if (person == 2) {
4066#line 222
4067                personOnFloor_2_3 = 1;
4068              } else {
4069#line 223
4070                if (person == 3) {
4071#line 224
4072                  personOnFloor_3_3 = 1;
4073                } else {
4074#line 225
4075                  if (person == 4) {
4076#line 226
4077                    personOnFloor_4_3 = 1;
4078                  } else {
4079#line 227
4080                    if (person == 5) {
4081#line 228
4082                      personOnFloor_5_3 = 1;
4083                    } else {
4084
4085                    }
4086                  }
4087                }
4088              }
4089            }
4090          }
4091        } else {
4092#line 229
4093          if (floor == 4) {
4094#line 224
4095            if (person == 0) {
4096#line 225
4097              personOnFloor_0_4 = 1;
4098            } else {
4099#line 226
4100              if (person == 1) {
4101#line 227
4102                personOnFloor_1_4 = 1;
4103              } else {
4104#line 228
4105                if (person == 2) {
4106#line 229
4107                  personOnFloor_2_4 = 1;
4108                } else {
4109#line 230
4110                  if (person == 3) {
4111#line 231
4112                    personOnFloor_3_4 = 1;
4113                  } else {
4114#line 232
4115                    if (person == 4) {
4116#line 233
4117                      personOnFloor_4_4 = 1;
4118                    } else {
4119#line 234
4120                      if (person == 5) {
4121#line 235
4122                        personOnFloor_5_4 = 1;
4123                      } else {
4124
4125                      }
4126                    }
4127                  }
4128                }
4129              }
4130            }
4131          } else {
4132
4133          }
4134        }
4135      }
4136    }
4137  }
4138  {
4139#line 225
4140  callOnFloor(floor);
4141  }
4142#line 1598 "Floor.c"
4143  return;
4144}
4145}
4146#line 228 "Floor.c"
4147void removePersonFromFloor(int person , int floor ) 
4148{ 
4149
4150  {
4151#line 265
4152  if (floor == 0) {
4153#line 236
4154    if (person == 0) {
4155#line 237
4156      personOnFloor_0_0 = 0;
4157    } else {
4158#line 238
4159      if (person == 1) {
4160#line 239
4161        personOnFloor_1_0 = 0;
4162      } else {
4163#line 240
4164        if (person == 2) {
4165#line 241
4166          personOnFloor_2_0 = 0;
4167        } else {
4168#line 242
4169          if (person == 3) {
4170#line 243
4171            personOnFloor_3_0 = 0;
4172          } else {
4173#line 244
4174            if (person == 4) {
4175#line 245
4176              personOnFloor_4_0 = 0;
4177            } else {
4178#line 246
4179              if (person == 5) {
4180#line 247
4181                personOnFloor_5_0 = 0;
4182              } else {
4183
4184              }
4185            }
4186          }
4187        }
4188      }
4189    }
4190  } else {
4191#line 248
4192    if (floor == 1) {
4193#line 243
4194      if (person == 0) {
4195#line 244
4196        personOnFloor_0_1 = 0;
4197      } else {
4198#line 245
4199        if (person == 1) {
4200#line 246
4201          personOnFloor_1_1 = 0;
4202        } else {
4203#line 247
4204          if (person == 2) {
4205#line 248
4206            personOnFloor_2_1 = 0;
4207          } else {
4208#line 249
4209            if (person == 3) {
4210#line 250
4211              personOnFloor_3_1 = 0;
4212            } else {
4213#line 251
4214              if (person == 4) {
4215#line 252
4216                personOnFloor_4_1 = 0;
4217              } else {
4218#line 253
4219                if (person == 5) {
4220#line 254
4221                  personOnFloor_5_1 = 0;
4222                } else {
4223
4224                }
4225              }
4226            }
4227          }
4228        }
4229      }
4230    } else {
4231#line 255
4232      if (floor == 2) {
4233#line 250
4234        if (person == 0) {
4235#line 251
4236          personOnFloor_0_2 = 0;
4237        } else {
4238#line 252
4239          if (person == 1) {
4240#line 253
4241            personOnFloor_1_2 = 0;
4242          } else {
4243#line 254
4244            if (person == 2) {
4245#line 255
4246              personOnFloor_2_2 = 0;
4247            } else {
4248#line 256
4249              if (person == 3) {
4250#line 257
4251                personOnFloor_3_2 = 0;
4252              } else {
4253#line 258
4254                if (person == 4) {
4255#line 259
4256                  personOnFloor_4_2 = 0;
4257                } else {
4258#line 260
4259                  if (person == 5) {
4260#line 261
4261                    personOnFloor_5_2 = 0;
4262                  } else {
4263
4264                  }
4265                }
4266              }
4267            }
4268          }
4269        }
4270      } else {
4271#line 262
4272        if (floor == 3) {
4273#line 257
4274          if (person == 0) {
4275#line 258
4276            personOnFloor_0_3 = 0;
4277          } else {
4278#line 259
4279            if (person == 1) {
4280#line 260
4281              personOnFloor_1_3 = 0;
4282            } else {
4283#line 261
4284              if (person == 2) {
4285#line 262
4286                personOnFloor_2_3 = 0;
4287              } else {
4288#line 263
4289                if (person == 3) {
4290#line 264
4291                  personOnFloor_3_3 = 0;
4292                } else {
4293#line 265
4294                  if (person == 4) {
4295#line 266
4296                    personOnFloor_4_3 = 0;
4297                  } else {
4298#line 267
4299                    if (person == 5) {
4300#line 268
4301                      personOnFloor_5_3 = 0;
4302                    } else {
4303
4304                    }
4305                  }
4306                }
4307              }
4308            }
4309          }
4310        } else {
4311#line 269
4312          if (floor == 4) {
4313#line 264
4314            if (person == 0) {
4315#line 265
4316              personOnFloor_0_4 = 0;
4317            } else {
4318#line 266
4319              if (person == 1) {
4320#line 267
4321                personOnFloor_1_4 = 0;
4322              } else {
4323#line 268
4324                if (person == 2) {
4325#line 269
4326                  personOnFloor_2_4 = 0;
4327                } else {
4328#line 270
4329                  if (person == 3) {
4330#line 271
4331                    personOnFloor_3_4 = 0;
4332                  } else {
4333#line 272
4334                    if (person == 4) {
4335#line 273
4336                      personOnFloor_4_4 = 0;
4337                    } else {
4338#line 274
4339                      if (person == 5) {
4340#line 275
4341                        personOnFloor_5_4 = 0;
4342                      } else {
4343
4344                      }
4345                    }
4346                  }
4347                }
4348              }
4349            }
4350          } else {
4351
4352          }
4353        }
4354      }
4355    }
4356  }
4357  {
4358#line 265
4359  resetCallOnFloor(floor);
4360  }
4361#line 1694 "Floor.c"
4362  return;
4363}
4364}
4365#line 268 "Floor.c"
4366int isTopFloor(int floorID ) 
4367{ int retValue_acc ;
4368
4369  {
4370#line 1712 "Floor.c"
4371  retValue_acc = floorID == 4;
4372#line 1714
4373  return (retValue_acc);
4374#line 1721
4375  return (retValue_acc);
4376}
4377}
4378#line 1 "featureselect.o"
4379#pragma merger(0,"featureselect.i","")
4380#line 9 "featureselect.h"
4381int select_one(void) ;
4382#line 8 "featureselect.c"
4383int select_one(void) 
4384{ int retValue_acc ;
4385  int choice = __VERIFIER_nondet_int();
4386
4387  {
4388#line 63 "featureselect.c"
4389  retValue_acc = choice;
4390#line 65
4391  return (retValue_acc);
4392#line 72
4393  return (retValue_acc);
4394}
4395}
4396#line 14 "featureselect.c"
4397void select_features(void) 
4398{ 
4399
4400  {
4401#line 94 "featureselect.c"
4402  return;
4403}
4404}
4405#line 20 "featureselect.c"
4406void select_helpers(void) 
4407{ 
4408
4409  {
4410#line 112 "featureselect.c"
4411  return;
4412}
4413}
4414#line 25 "featureselect.c"
4415int valid_product(void) 
4416{ int retValue_acc ;
4417
4418  {
4419#line 130 "featureselect.c"
4420  retValue_acc = 1;
4421#line 132
4422  return (retValue_acc);
4423#line 139
4424  return (retValue_acc);
4425}
4426}
4427#line 1 "libacc.o"
4428#pragma merger(0,"libacc.i","")
4429#line 73 "/usr/include/assert.h"
4430extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
4431                                                                      char const   *__file ,
4432                                                                      unsigned int __line ,
4433                                                                      char const   *__function ) ;
4434#line 471 "/usr/include/stdlib.h"
4435extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
4436#line 488
4437extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
4438#line 32 "libacc.c"
4439void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
4440                                                                           int  ) ,
4441                                       int val ) 
4442{ struct __UTAC__EXCEPTION *excep ;
4443  struct __UTAC__CFLOW_FUNC *cf ;
4444  void *tmp ;
4445  unsigned long __cil_tmp7 ;
4446  unsigned long __cil_tmp8 ;
4447  unsigned long __cil_tmp9 ;
4448  unsigned long __cil_tmp10 ;
4449  unsigned long __cil_tmp11 ;
4450  unsigned long __cil_tmp12 ;
4451  unsigned long __cil_tmp13 ;
4452  unsigned long __cil_tmp14 ;
4453  int (**mem_15)(int  , int  ) ;
4454  int *mem_16 ;
4455  struct __UTAC__CFLOW_FUNC **mem_17 ;
4456  struct __UTAC__CFLOW_FUNC **mem_18 ;
4457  struct __UTAC__CFLOW_FUNC **mem_19 ;
4458
4459  {
4460  {
4461#line 33
4462  excep = (struct __UTAC__EXCEPTION *)exception;
4463#line 34
4464  tmp = malloc(24UL);
4465#line 34
4466  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
4467#line 36
4468  mem_15 = (int (**)(int  , int  ))cf;
4469#line 36
4470  *mem_15 = cflow_func;
4471#line 37
4472  __cil_tmp7 = (unsigned long )cf;
4473#line 37
4474  __cil_tmp8 = __cil_tmp7 + 8;
4475#line 37
4476  mem_16 = (int *)__cil_tmp8;
4477#line 37
4478  *mem_16 = val;
4479#line 38
4480  __cil_tmp9 = (unsigned long )cf;
4481#line 38
4482  __cil_tmp10 = __cil_tmp9 + 16;
4483#line 38
4484  __cil_tmp11 = (unsigned long )excep;
4485#line 38
4486  __cil_tmp12 = __cil_tmp11 + 24;
4487#line 38
4488  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
4489#line 38
4490  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
4491#line 38
4492  *mem_17 = *mem_18;
4493#line 39
4494  __cil_tmp13 = (unsigned long )excep;
4495#line 39
4496  __cil_tmp14 = __cil_tmp13 + 24;
4497#line 39
4498  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4499#line 39
4500  *mem_19 = cf;
4501  }
4502#line 654 "libacc.c"
4503  return;
4504}
4505}
4506#line 44 "libacc.c"
4507void __utac__exception__cf_handler_free(void *exception ) 
4508{ struct __UTAC__EXCEPTION *excep ;
4509  struct __UTAC__CFLOW_FUNC *cf ;
4510  struct __UTAC__CFLOW_FUNC *tmp ;
4511  unsigned long __cil_tmp5 ;
4512  unsigned long __cil_tmp6 ;
4513  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4514  unsigned long __cil_tmp8 ;
4515  unsigned long __cil_tmp9 ;
4516  unsigned long __cil_tmp10 ;
4517  unsigned long __cil_tmp11 ;
4518  void *__cil_tmp12 ;
4519  unsigned long __cil_tmp13 ;
4520  unsigned long __cil_tmp14 ;
4521  struct __UTAC__CFLOW_FUNC **mem_15 ;
4522  struct __UTAC__CFLOW_FUNC **mem_16 ;
4523  struct __UTAC__CFLOW_FUNC **mem_17 ;
4524
4525  {
4526#line 45
4527  excep = (struct __UTAC__EXCEPTION *)exception;
4528#line 46
4529  __cil_tmp5 = (unsigned long )excep;
4530#line 46
4531  __cil_tmp6 = __cil_tmp5 + 24;
4532#line 46
4533  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4534#line 46
4535  cf = *mem_15;
4536  {
4537#line 49
4538  while (1) {
4539    while_7_continue: /* CIL Label */ ;
4540    {
4541#line 49
4542    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4543#line 49
4544    __cil_tmp8 = (unsigned long )__cil_tmp7;
4545#line 49
4546    __cil_tmp9 = (unsigned long )cf;
4547#line 49
4548    if (__cil_tmp9 != __cil_tmp8) {
4549
4550    } else {
4551      goto while_7_break;
4552    }
4553    }
4554    {
4555#line 50
4556    tmp = cf;
4557#line 51
4558    __cil_tmp10 = (unsigned long )cf;
4559#line 51
4560    __cil_tmp11 = __cil_tmp10 + 16;
4561#line 51
4562    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
4563#line 51
4564    cf = *mem_16;
4565#line 52
4566    __cil_tmp12 = (void *)tmp;
4567#line 52
4568    free(__cil_tmp12);
4569    }
4570  }
4571  while_7_break: /* CIL Label */ ;
4572  }
4573#line 55
4574  __cil_tmp13 = (unsigned long )excep;
4575#line 55
4576  __cil_tmp14 = __cil_tmp13 + 24;
4577#line 55
4578  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
4579#line 55
4580  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
4581#line 694 "libacc.c"
4582  return;
4583}
4584}
4585#line 59 "libacc.c"
4586void __utac__exception__cf_handler_reset(void *exception ) 
4587{ struct __UTAC__EXCEPTION *excep ;
4588  struct __UTAC__CFLOW_FUNC *cf ;
4589  unsigned long __cil_tmp5 ;
4590  unsigned long __cil_tmp6 ;
4591  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
4592  unsigned long __cil_tmp8 ;
4593  unsigned long __cil_tmp9 ;
4594  int (*__cil_tmp10)(int  , int  ) ;
4595  unsigned long __cil_tmp11 ;
4596  unsigned long __cil_tmp12 ;
4597  int __cil_tmp13 ;
4598  unsigned long __cil_tmp14 ;
4599  unsigned long __cil_tmp15 ;
4600  struct __UTAC__CFLOW_FUNC **mem_16 ;
4601  int (**mem_17)(int  , int  ) ;
4602  int *mem_18 ;
4603  struct __UTAC__CFLOW_FUNC **mem_19 ;
4604
4605  {
4606#line 60
4607  excep = (struct __UTAC__EXCEPTION *)exception;
4608#line 61
4609  __cil_tmp5 = (unsigned long )excep;
4610#line 61
4611  __cil_tmp6 = __cil_tmp5 + 24;
4612#line 61
4613  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
4614#line 61
4615  cf = *mem_16;
4616  {
4617#line 64
4618  while (1) {
4619    while_8_continue: /* CIL Label */ ;
4620    {
4621#line 64
4622    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
4623#line 64
4624    __cil_tmp8 = (unsigned long )__cil_tmp7;
4625#line 64
4626    __cil_tmp9 = (unsigned long )cf;
4627#line 64
4628    if (__cil_tmp9 != __cil_tmp8) {
4629
4630    } else {
4631      goto while_8_break;
4632    }
4633    }
4634    {
4635#line 65
4636    mem_17 = (int (**)(int  , int  ))cf;
4637#line 65
4638    __cil_tmp10 = *mem_17;
4639#line 65
4640    __cil_tmp11 = (unsigned long )cf;
4641#line 65
4642    __cil_tmp12 = __cil_tmp11 + 8;
4643#line 65
4644    mem_18 = (int *)__cil_tmp12;
4645#line 65
4646    __cil_tmp13 = *mem_18;
4647#line 65
4648    (*__cil_tmp10)(4, __cil_tmp13);
4649#line 66
4650    __cil_tmp14 = (unsigned long )cf;
4651#line 66
4652    __cil_tmp15 = __cil_tmp14 + 16;
4653#line 66
4654    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
4655#line 66
4656    cf = *mem_19;
4657    }
4658  }
4659  while_8_break: /* CIL Label */ ;
4660  }
4661  {
4662#line 69
4663  __utac__exception__cf_handler_free(exception);
4664  }
4665#line 732 "libacc.c"
4666  return;
4667}
4668}
4669#line 80 "libacc.c"
4670void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
4671#line 80 "libacc.c"
4672static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
4673#line 79 "libacc.c"
4674void *__utac__error_stack_mgt(void *env , int mode , int count ) 
4675{ void *retValue_acc ;
4676  struct __ACC__ERR *new ;
4677  void *tmp ;
4678  struct __ACC__ERR *temp ;
4679  struct __ACC__ERR *next ;
4680  void *excep ;
4681  unsigned long __cil_tmp10 ;
4682  unsigned long __cil_tmp11 ;
4683  unsigned long __cil_tmp12 ;
4684  unsigned long __cil_tmp13 ;
4685  void *__cil_tmp14 ;
4686  unsigned long __cil_tmp15 ;
4687  unsigned long __cil_tmp16 ;
4688  void *__cil_tmp17 ;
4689  void **mem_18 ;
4690  struct __ACC__ERR **mem_19 ;
4691  struct __ACC__ERR **mem_20 ;
4692  void **mem_21 ;
4693  struct __ACC__ERR **mem_22 ;
4694  void **mem_23 ;
4695  void **mem_24 ;
4696
4697  {
4698#line 82 "libacc.c"
4699  if (count == 0) {
4700#line 758 "libacc.c"
4701    return (retValue_acc);
4702  } else {
4703
4704  }
4705#line 86 "libacc.c"
4706  if (mode == 0) {
4707    {
4708#line 87
4709    tmp = malloc(16UL);
4710#line 87
4711    new = (struct __ACC__ERR *)tmp;
4712#line 88
4713    mem_18 = (void **)new;
4714#line 88
4715    *mem_18 = env;
4716#line 89
4717    __cil_tmp10 = (unsigned long )new;
4718#line 89
4719    __cil_tmp11 = __cil_tmp10 + 8;
4720#line 89
4721    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
4722#line 89
4723    *mem_19 = head;
4724#line 90
4725    head = new;
4726#line 776 "libacc.c"
4727    retValue_acc = (void *)new;
4728    }
4729#line 778
4730    return (retValue_acc);
4731  } else {
4732
4733  }
4734#line 94 "libacc.c"
4735  if (mode == 1) {
4736#line 95
4737    temp = head;
4738    {
4739#line 98
4740    while (1) {
4741      while_9_continue: /* CIL Label */ ;
4742#line 98
4743      if (count > 1) {
4744
4745      } else {
4746        goto while_9_break;
4747      }
4748      {
4749#line 99
4750      __cil_tmp12 = (unsigned long )temp;
4751#line 99
4752      __cil_tmp13 = __cil_tmp12 + 8;
4753#line 99
4754      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
4755#line 99
4756      next = *mem_20;
4757#line 100
4758      mem_21 = (void **)temp;
4759#line 100
4760      excep = *mem_21;
4761#line 101
4762      __cil_tmp14 = (void *)temp;
4763#line 101
4764      free(__cil_tmp14);
4765#line 102
4766      __utac__exception__cf_handler_reset(excep);
4767#line 103
4768      temp = next;
4769#line 104
4770      count = count - 1;
4771      }
4772    }
4773    while_9_break: /* CIL Label */ ;
4774    }
4775    {
4776#line 107
4777    __cil_tmp15 = (unsigned long )temp;
4778#line 107
4779    __cil_tmp16 = __cil_tmp15 + 8;
4780#line 107
4781    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
4782#line 107
4783    head = *mem_22;
4784#line 108
4785    mem_23 = (void **)temp;
4786#line 108
4787    excep = *mem_23;
4788#line 109
4789    __cil_tmp17 = (void *)temp;
4790#line 109
4791    free(__cil_tmp17);
4792#line 110
4793    __utac__exception__cf_handler_reset(excep);
4794#line 820 "libacc.c"
4795    retValue_acc = excep;
4796    }
4797#line 822
4798    return (retValue_acc);
4799  } else {
4800
4801  }
4802#line 114
4803  if (mode == 2) {
4804#line 118 "libacc.c"
4805    if (head) {
4806#line 831
4807      mem_24 = (void **)head;
4808#line 831
4809      retValue_acc = *mem_24;
4810#line 833
4811      return (retValue_acc);
4812    } else {
4813#line 837 "libacc.c"
4814      retValue_acc = (void *)0;
4815#line 839
4816      return (retValue_acc);
4817    }
4818  } else {
4819
4820  }
4821#line 846 "libacc.c"
4822  return (retValue_acc);
4823}
4824}
4825#line 122 "libacc.c"
4826void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
4827{ void *retValue_acc ;
4828  unsigned long __cil_tmp4 ;
4829  unsigned long __cil_tmp5 ;
4830  int __cil_tmp6 ;
4831  int __cil_tmp7 ;
4832  unsigned long __cil_tmp8 ;
4833  unsigned long __cil_tmp9 ;
4834  void **__cil_tmp10 ;
4835  void **__cil_tmp11 ;
4836  int *mem_12 ;
4837  void ***mem_13 ;
4838
4839  {
4840#line 123
4841  if (i > 0) {
4842    {
4843#line 123
4844    __cil_tmp4 = (unsigned long )this;
4845#line 123
4846    __cil_tmp5 = __cil_tmp4 + 16;
4847#line 123
4848    mem_12 = (int *)__cil_tmp5;
4849#line 123
4850    __cil_tmp6 = *mem_12;
4851#line 123
4852    if (i <= __cil_tmp6) {
4853
4854    } else {
4855      {
4856#line 123
4857      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4858                    123U, "__utac__get_this_arg");
4859      }
4860    }
4861    }
4862  } else {
4863    {
4864#line 123
4865    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4866                  123U, "__utac__get_this_arg");
4867    }
4868  }
4869#line 870 "libacc.c"
4870  __cil_tmp7 = i - 1;
4871#line 870
4872  __cil_tmp8 = (unsigned long )this;
4873#line 870
4874  __cil_tmp9 = __cil_tmp8 + 8;
4875#line 870
4876  mem_13 = (void ***)__cil_tmp9;
4877#line 870
4878  __cil_tmp10 = *mem_13;
4879#line 870
4880  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4881#line 870
4882  retValue_acc = *__cil_tmp11;
4883#line 872
4884  return (retValue_acc);
4885#line 879
4886  return (retValue_acc);
4887}
4888}
4889#line 129 "libacc.c"
4890char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
4891{ char const   *retValue_acc ;
4892  unsigned long __cil_tmp4 ;
4893  unsigned long __cil_tmp5 ;
4894  int __cil_tmp6 ;
4895  int __cil_tmp7 ;
4896  unsigned long __cil_tmp8 ;
4897  unsigned long __cil_tmp9 ;
4898  char const   **__cil_tmp10 ;
4899  char const   **__cil_tmp11 ;
4900  int *mem_12 ;
4901  char const   ***mem_13 ;
4902
4903  {
4904#line 131
4905  if (i > 0) {
4906    {
4907#line 131
4908    __cil_tmp4 = (unsigned long )this;
4909#line 131
4910    __cil_tmp5 = __cil_tmp4 + 16;
4911#line 131
4912    mem_12 = (int *)__cil_tmp5;
4913#line 131
4914    __cil_tmp6 = *mem_12;
4915#line 131
4916    if (i <= __cil_tmp6) {
4917
4918    } else {
4919      {
4920#line 131
4921      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4922                    131U, "__utac__get_this_argtype");
4923      }
4924    }
4925    }
4926  } else {
4927    {
4928#line 131
4929    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4930                  131U, "__utac__get_this_argtype");
4931    }
4932  }
4933#line 903 "libacc.c"
4934  __cil_tmp7 = i - 1;
4935#line 903
4936  __cil_tmp8 = (unsigned long )this;
4937#line 903
4938  __cil_tmp9 = __cil_tmp8 + 24;
4939#line 903
4940  mem_13 = (char const   ***)__cil_tmp9;
4941#line 903
4942  __cil_tmp10 = *mem_13;
4943#line 903
4944  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4945#line 903
4946  retValue_acc = *__cil_tmp11;
4947#line 905
4948  return (retValue_acc);
4949#line 912
4950  return (retValue_acc);
4951}
4952}
4953#line 1 "wsllib_check.o"
4954#pragma merger(0,"wsllib_check.i","")
4955#line 3 "wsllib_check.c"
4956void __automaton_fail(void) 
4957{ 
4958
4959  {
4960  goto ERROR;
4961  ERROR: ;
4962#line 53 "wsllib_check.c"
4963  return;
4964}
4965}
↑