Showing error 1585

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