Showing error 1606

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