Showing error 1622

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