Showing error 1595

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