Showing error 1628

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