Showing error 1875

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/minepump_spec1_product35_unsafe.cil.c
Line in file: 198
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);
   2extern int printf (__const char *__restrict __format, ...);
   3/* Generated by CIL v. 1.3.7 */
   4/* print_CIL_Input is true */
   5
   6#line 2 "libacc.c"
   7struct JoinPoint {
   8   void **(*fp)(struct JoinPoint * ) ;
   9   void **args ;
  10   int argsCount ;
  11   char const   **argsType ;
  12   void *(*arg)(int  , struct JoinPoint * ) ;
  13   char const   *(*argType)(int  , struct JoinPoint * ) ;
  14   void **retValue ;
  15   char const   *retType ;
  16   char const   *funcName ;
  17   char const   *targetName ;
  18   char const   *fileName ;
  19   char const   *kind ;
  20   void *excep_return ;
  21};
  22#line 18 "libacc.c"
  23struct __UTAC__CFLOW_FUNC {
  24   int (*func)(int  , int  ) ;
  25   int val ;
  26   struct __UTAC__CFLOW_FUNC *next ;
  27};
  28#line 18 "libacc.c"
  29struct __UTAC__EXCEPTION {
  30   void *jumpbuf ;
  31   unsigned long long prtValue ;
  32   int pops ;
  33   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
  34};
  35#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
  36typedef unsigned long size_t;
  37#line 76 "libacc.c"
  38struct __ACC__ERR {
  39   void *v ;
  40   struct __ACC__ERR *next ;
  41};
  42#line 1 "Environment.o"
  43#pragma merger(0,"Environment.i","")
  44#line 4 "Environment.h"
  45void lowerWaterLevel(void) ;
  46#line 6
  47void waterRise(void) ;
  48#line 8
  49void changeMethaneLevel(void) ;
  50#line 10
  51int isMethaneLevelCritical(void) ;
  52#line 12
  53int getWaterLevel(void) ;
  54#line 15
  55void printEnvironment(void) ;
  56#line 16
  57int isHighWaterSensorDry(void) ;
  58#line 9 "Environment.c"
  59int waterLevel  =    1;
  60#line 12 "Environment.c"
  61int methaneLevelCritical  =    0;
  62#line 15 "Environment.c"
  63void lowerWaterLevel(void) 
  64{ 
  65
  66  {
  67#line 19
  68  if (waterLevel > 0) {
  69#line 17
  70    waterLevel = waterLevel - 1;
  71  } else {
  72
  73  }
  74#line 83 "Environment.c"
  75  return;
  76}
  77}
  78#line 22 "Environment.c"
  79void waterRise(void) 
  80{ 
  81
  82  {
  83#line 26
  84  if (waterLevel < 2) {
  85#line 24
  86    waterLevel = waterLevel + 1;
  87  } else {
  88
  89  }
  90#line 106 "Environment.c"
  91  return;
  92}
  93}
  94#line 29 "Environment.c"
  95void changeMethaneLevel(void) 
  96{ 
  97
  98  {
  99#line 34
 100  if (methaneLevelCritical) {
 101#line 31
 102    methaneLevelCritical = 0;
 103  } else {
 104#line 33
 105    methaneLevelCritical = 1;
 106  }
 107#line 132 "Environment.c"
 108  return;
 109}
 110}
 111#line 38 "Environment.c"
 112int isMethaneLevelCritical(void) 
 113{ int retValue_acc ;
 114
 115  {
 116#line 150 "Environment.c"
 117  retValue_acc = methaneLevelCritical;
 118#line 152
 119  return (retValue_acc);
 120#line 159
 121  return (retValue_acc);
 122}
 123}
 124#line 45 "Environment.c"
 125#line 44 "Environment.c"
 126void printEnvironment(void) 
 127{ 
 128
 129  {
 130  {
 131#line 45
 132  printf("Env(Water:%i", waterLevel);
 133#line 46
 134  printf(",Meth:");
 135  }
 136#line 47
 137  if (methaneLevelCritical) {
 138    {
 139#line 48
 140    printf("CRIT");
 141    }
 142  } else {
 143    {
 144#line 49
 145    printf("OK");
 146    }
 147  }
 148  {
 149#line 51
 150  printf(")");
 151  }
 152#line 191 "Environment.c"
 153  return;
 154}
 155}
 156#line 55 "Environment.c"
 157int getWaterLevel(void) 
 158{ int retValue_acc ;
 159
 160  {
 161#line 209 "Environment.c"
 162  retValue_acc = waterLevel;
 163#line 211
 164  return (retValue_acc);
 165#line 218
 166  return (retValue_acc);
 167}
 168}
 169#line 58 "Environment.c"
 170int isHighWaterSensorDry(void) 
 171{ int retValue_acc ;
 172
 173  {
 174#line 65 "Environment.c"
 175  if (waterLevel < 2) {
 176#line 243
 177    retValue_acc = 1;
 178#line 245
 179    return (retValue_acc);
 180  } else {
 181#line 251 "Environment.c"
 182    retValue_acc = 0;
 183#line 253
 184    return (retValue_acc);
 185  }
 186#line 260 "Environment.c"
 187  return (retValue_acc);
 188}
 189}
 190#line 1 "wsllib_check.o"
 191#pragma merger(0,"wsllib_check.i","")
 192#line 3 "wsllib_check.c"
 193void __automaton_fail(void) 
 194{ 
 195
 196  {
 197  goto ERROR;
 198  ERROR: ;
 199#line 53 "wsllib_check.c"
 200  return;
 201}
 202}
 203#line 1 "Specification1_spec.o"
 204#pragma merger(0,"Specification1_spec.i","")
 205#line 10 "MinePump.h"
 206int isPumpRunning(void) ;
 207#line 11 "Specification1_spec.c"
 208__inline void __utac_acc__Specification1_spec__1(void) 
 209{ int tmp ;
 210  int tmp___0 ;
 211
 212  {
 213  {
 214#line 17
 215  tmp = isMethaneLevelCritical();
 216  }
 217#line 17
 218  if (tmp) {
 219    {
 220#line 17
 221    tmp___0 = isPumpRunning();
 222    }
 223#line 17
 224    if (tmp___0) {
 225      {
 226#line 14
 227      __automaton_fail();
 228      }
 229    } else {
 230
 231    }
 232  } else {
 233
 234  }
 235#line 14
 236  return;
 237}
 238}
 239#line 1 "scenario.o"
 240#pragma merger(0,"scenario.i","")
 241#line 7 "scenario.c"
 242#line 12
 243void stopSystem(void) ;
 244#line 14
 245void timeShift(void) ;
 246#line 16
 247void cleanup(void) ;
 248#line 1 "scenario.c"
 249void test(void) 
 250{ int splverifierCounter ;
 251  int tmp ;
 252  int tmp___0 ;
 253  int tmp___1 ;
 254  int tmp___2 ;
 255
 256  {
 257#line 2
 258  splverifierCounter = 0;
 259  {
 260#line 3
 261  while (1) {
 262    while_0_continue: /* CIL Label */ ;
 263#line 3
 264    if (splverifierCounter < 4) {
 265
 266    } else {
 267      goto while_0_break;
 268    }
 269    {
 270#line 7
 271    tmp = __VERIFIER_nondet_int();
 272    }
 273#line 7
 274    if (tmp) {
 275      {
 276#line 5
 277      waterRise();
 278      }
 279    } else {
 280
 281    }
 282    {
 283#line 7
 284    tmp___0 = __VERIFIER_nondet_int();
 285    }
 286#line 7
 287    if (tmp___0) {
 288      {
 289#line 8
 290      changeMethaneLevel();
 291      }
 292    } else {
 293
 294    }
 295    {
 296#line 10
 297    tmp___2 = __VERIFIER_nondet_int();
 298    }
 299#line 10
 300    if (tmp___2) {
 301
 302    } else {
 303      {
 304#line 12
 305      tmp___1 = __VERIFIER_nondet_int();
 306      }
 307#line 12
 308      if (tmp___1) {
 309        {
 310#line 12
 311        stopSystem();
 312        }
 313      } else {
 314
 315      }
 316    }
 317    {
 318#line 14
 319    timeShift();
 320    }
 321  }
 322  while_0_break: /* CIL Label */ ;
 323  }
 324  {
 325#line 16
 326  cleanup();
 327  }
 328#line 76 "scenario.c"
 329  return;
 330}
 331}
 332#line 1 "MinePump.o"
 333#pragma merger(0,"MinePump.i","")
 334#line 6 "MinePump.h"
 335void activatePump(void) ;
 336#line 8
 337void deactivatePump(void) ;
 338#line 13
 339void printPump(void) ;
 340#line 7 "MinePump.c"
 341int pumpRunning  =    0;
 342#line 9 "MinePump.c"
 343int systemActive  =    1;
 344#line 16
 345void processEnvironment(void) ;
 346#line 12 "MinePump.c"
 347void timeShift(void) 
 348{ 
 349
 350  {
 351#line 15
 352  if (pumpRunning) {
 353    {
 354#line 16
 355    lowerWaterLevel();
 356    }
 357  } else {
 358
 359  }
 360#line 15
 361  if (systemActive) {
 362    {
 363#line 16
 364    processEnvironment();
 365    }
 366  } else {
 367
 368  }
 369  {
 370#line 99 "MinePump.c"
 371  __utac_acc__Specification1_spec__1();
 372  }
 373#line 105
 374  return;
 375}
 376}
 377#line 19 "MinePump.c"
 378void processEnvironment__wrappee__base(void) 
 379{ 
 380
 381  {
 382#line 123 "MinePump.c"
 383  return;
 384}
 385}
 386#line 28 "MinePump.c"
 387int isHighWaterLevel(void) ;
 388#line 23 "MinePump.c"
 389void processEnvironment(void) 
 390{ int tmp ;
 391
 392  {
 393#line 28
 394  if (! pumpRunning) {
 395    {
 396#line 28
 397    tmp = isHighWaterLevel();
 398    }
 399#line 28
 400    if (tmp) {
 401      {
 402#line 25
 403      activatePump();
 404      }
 405    } else {
 406      {
 407#line 27
 408      processEnvironment__wrappee__base();
 409      }
 410    }
 411  } else {
 412    {
 413#line 27
 414    processEnvironment__wrappee__base();
 415    }
 416  }
 417#line 149 "MinePump.c"
 418  return;
 419}
 420}
 421#line 32 "MinePump.c"
 422void activatePump(void) 
 423{ 
 424
 425  {
 426#line 33
 427  pumpRunning = 1;
 428#line 169 "MinePump.c"
 429  return;
 430}
 431}
 432#line 37 "MinePump.c"
 433void deactivatePump(void) 
 434{ 
 435
 436  {
 437#line 38
 438  pumpRunning = 0;
 439#line 189 "MinePump.c"
 440  return;
 441}
 442}
 443#line 42 "MinePump.c"
 444int isMethaneAlarm(void) 
 445{ int retValue_acc ;
 446
 447  {
 448  {
 449#line 207 "MinePump.c"
 450  retValue_acc = isMethaneLevelCritical();
 451  }
 452#line 209
 453  return (retValue_acc);
 454#line 216
 455  return (retValue_acc);
 456}
 457}
 458#line 47 "MinePump.c"
 459int isPumpRunning(void) 
 460{ int retValue_acc ;
 461
 462  {
 463#line 238 "MinePump.c"
 464  retValue_acc = pumpRunning;
 465#line 240
 466  return (retValue_acc);
 467#line 247
 468  return (retValue_acc);
 469}
 470}
 471#line 52 "MinePump.c"
 472void printPump(void) 
 473{ 
 474
 475  {
 476  {
 477#line 53
 478  printf("Pump(System:");
 479  }
 480#line 54
 481  if (systemActive) {
 482    {
 483#line 55
 484    printf("On");
 485    }
 486  } else {
 487    {
 488#line 56
 489    printf("Off");
 490    }
 491  }
 492  {
 493#line 58
 494  printf(",Pump:");
 495  }
 496#line 59
 497  if (pumpRunning) {
 498    {
 499#line 60
 500    printf("On");
 501    }
 502  } else {
 503    {
 504#line 61
 505    printf("Off");
 506    }
 507  }
 508  {
 509#line 63
 510  printf(") ");
 511#line 64
 512  printEnvironment();
 513#line 65
 514  printf("\n");
 515  }
 516#line 287 "MinePump.c"
 517  return;
 518}
 519}
 520#line 67 "MinePump.c"
 521int isHighWaterLevel(void) 
 522{ int retValue_acc ;
 523  int tmp ;
 524  int tmp___0 ;
 525
 526  {
 527  {
 528#line 305 "MinePump.c"
 529  tmp = isHighWaterSensorDry();
 530  }
 531#line 305
 532  if (tmp) {
 533#line 305
 534    tmp___0 = 0;
 535  } else {
 536#line 305
 537    tmp___0 = 1;
 538  }
 539#line 305
 540  retValue_acc = tmp___0;
 541#line 307
 542  return (retValue_acc);
 543#line 314
 544  return (retValue_acc);
 545}
 546}
 547#line 70 "MinePump.c"
 548void stopSystem(void) 
 549{ 
 550
 551  {
 552#line 75
 553  if (pumpRunning) {
 554    {
 555#line 72
 556    deactivatePump();
 557    }
 558  } else {
 559
 560  }
 561#line 75
 562  systemActive = 0;
 563#line 343 "MinePump.c"
 564  return;
 565}
 566}
 567#line 1 "featureselect.o"
 568#pragma merger(0,"featureselect.i","")
 569#line 8 "featureselect.h"
 570int select_one(void) ;
 571#line 10
 572void select_features(void) ;
 573#line 12
 574void select_helpers(void) ;
 575#line 14
 576int valid_product(void) ;
 577#line 8 "featureselect.c"
 578int select_one(void) 
 579{ int retValue_acc ;
 580  int choice = __VERIFIER_nondet_int();
 581
 582  {
 583#line 62 "featureselect.c"
 584  retValue_acc = choice;
 585#line 64
 586  return (retValue_acc);
 587#line 71
 588  return (retValue_acc);
 589}
 590}
 591#line 14 "featureselect.c"
 592void select_features(void) 
 593{ 
 594
 595  {
 596#line 93 "featureselect.c"
 597  return;
 598}
 599}
 600#line 20 "featureselect.c"
 601void select_helpers(void) 
 602{ 
 603
 604  {
 605#line 111 "featureselect.c"
 606  return;
 607}
 608}
 609#line 25 "featureselect.c"
 610int valid_product(void) 
 611{ int retValue_acc ;
 612
 613  {
 614#line 129 "featureselect.c"
 615  retValue_acc = 1;
 616#line 131
 617  return (retValue_acc);
 618#line 138
 619  return (retValue_acc);
 620}
 621}
 622#line 1 "Test.o"
 623#pragma merger(0,"Test.i","")
 624#line 8 "Test.c"
 625int cleanupTimeShifts  =    4;
 626#line 11 "Test.c"
 627#line 17 "Test.c"
 628void cleanup(void) 
 629{ int i ;
 630  int __cil_tmp2 ;
 631
 632  {
 633  {
 634#line 20
 635  timeShift();
 636#line 22
 637  i = 0;
 638  }
 639  {
 640#line 22
 641  while (1) {
 642    while_1_continue: /* CIL Label */ ;
 643    {
 644#line 22
 645    __cil_tmp2 = cleanupTimeShifts - 1;
 646#line 22
 647    if (i < __cil_tmp2) {
 648
 649    } else {
 650      goto while_1_break;
 651    }
 652    }
 653    {
 654#line 23
 655    timeShift();
 656#line 22
 657    i = i + 1;
 658    }
 659  }
 660  while_1_break: /* CIL Label */ ;
 661  }
 662#line 1111 "Test.c"
 663  return;
 664}
 665}
 666#line 56 "Test.c"
 667void Specification2(void) 
 668{ 
 669
 670  {
 671  {
 672#line 57
 673  timeShift();
 674#line 57
 675  printPump();
 676#line 58
 677  timeShift();
 678#line 58
 679  printPump();
 680#line 59
 681  timeShift();
 682#line 59
 683  printPump();
 684#line 60
 685  waterRise();
 686#line 60
 687  printPump();
 688#line 61
 689  timeShift();
 690#line 61
 691  printPump();
 692#line 62
 693  changeMethaneLevel();
 694#line 62
 695  printPump();
 696#line 63
 697  timeShift();
 698#line 63
 699  printPump();
 700#line 64
 701  cleanup();
 702  }
 703#line 1159 "Test.c"
 704  return;
 705}
 706}
 707#line 67 "Test.c"
 708void setup(void) 
 709{ 
 710
 711  {
 712#line 1177 "Test.c"
 713  return;
 714}
 715}
 716#line 74 "Test.c"
 717void runTest(void) 
 718{ 
 719
 720  {
 721  {
 722#line 77
 723  test();
 724  }
 725#line 1197 "Test.c"
 726  return;
 727}
 728}
 729#line 82 "Test.c"
 730int main(void) 
 731{ int retValue_acc ;
 732  int tmp ;
 733
 734  {
 735  {
 736#line 83
 737  select_helpers();
 738#line 84
 739  select_features();
 740#line 85
 741  tmp = valid_product();
 742  }
 743#line 85
 744  if (tmp) {
 745    {
 746#line 86
 747    setup();
 748#line 87
 749    runTest();
 750    }
 751  } else {
 752
 753  }
 754#line 1226 "Test.c"
 755  retValue_acc = 0;
 756#line 1228
 757  return (retValue_acc);
 758#line 1235
 759  return (retValue_acc);
 760}
 761}
 762#line 1 "libacc.o"
 763#pragma merger(0,"libacc.i","")
 764#line 73 "/usr/include/assert.h"
 765extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 766                                                                      char const   *__file ,
 767                                                                      unsigned int __line ,
 768                                                                      char const   *__function ) ;
 769#line 471 "/usr/include/stdlib.h"
 770extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 771#line 488
 772extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
 773#line 32 "libacc.c"
 774void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
 775                                                                           int  ) ,
 776                                       int val ) 
 777{ struct __UTAC__EXCEPTION *excep ;
 778  struct __UTAC__CFLOW_FUNC *cf ;
 779  void *tmp ;
 780  unsigned long __cil_tmp7 ;
 781  unsigned long __cil_tmp8 ;
 782  unsigned long __cil_tmp9 ;
 783  unsigned long __cil_tmp10 ;
 784  unsigned long __cil_tmp11 ;
 785  unsigned long __cil_tmp12 ;
 786  unsigned long __cil_tmp13 ;
 787  unsigned long __cil_tmp14 ;
 788  int (**mem_15)(int  , int  ) ;
 789  int *mem_16 ;
 790  struct __UTAC__CFLOW_FUNC **mem_17 ;
 791  struct __UTAC__CFLOW_FUNC **mem_18 ;
 792  struct __UTAC__CFLOW_FUNC **mem_19 ;
 793
 794  {
 795  {
 796#line 33
 797  excep = (struct __UTAC__EXCEPTION *)exception;
 798#line 34
 799  tmp = malloc(24UL);
 800#line 34
 801  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
 802#line 36
 803  mem_15 = (int (**)(int  , int  ))cf;
 804#line 36
 805  *mem_15 = cflow_func;
 806#line 37
 807  __cil_tmp7 = (unsigned long )cf;
 808#line 37
 809  __cil_tmp8 = __cil_tmp7 + 8;
 810#line 37
 811  mem_16 = (int *)__cil_tmp8;
 812#line 37
 813  *mem_16 = val;
 814#line 38
 815  __cil_tmp9 = (unsigned long )cf;
 816#line 38
 817  __cil_tmp10 = __cil_tmp9 + 16;
 818#line 38
 819  __cil_tmp11 = (unsigned long )excep;
 820#line 38
 821  __cil_tmp12 = __cil_tmp11 + 24;
 822#line 38
 823  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
 824#line 38
 825  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
 826#line 38
 827  *mem_17 = *mem_18;
 828#line 39
 829  __cil_tmp13 = (unsigned long )excep;
 830#line 39
 831  __cil_tmp14 = __cil_tmp13 + 24;
 832#line 39
 833  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
 834#line 39
 835  *mem_19 = cf;
 836  }
 837#line 654 "libacc.c"
 838  return;
 839}
 840}
 841#line 44 "libacc.c"
 842void __utac__exception__cf_handler_free(void *exception ) 
 843{ struct __UTAC__EXCEPTION *excep ;
 844  struct __UTAC__CFLOW_FUNC *cf ;
 845  struct __UTAC__CFLOW_FUNC *tmp ;
 846  unsigned long __cil_tmp5 ;
 847  unsigned long __cil_tmp6 ;
 848  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
 849  unsigned long __cil_tmp8 ;
 850  unsigned long __cil_tmp9 ;
 851  unsigned long __cil_tmp10 ;
 852  unsigned long __cil_tmp11 ;
 853  void *__cil_tmp12 ;
 854  unsigned long __cil_tmp13 ;
 855  unsigned long __cil_tmp14 ;
 856  struct __UTAC__CFLOW_FUNC **mem_15 ;
 857  struct __UTAC__CFLOW_FUNC **mem_16 ;
 858  struct __UTAC__CFLOW_FUNC **mem_17 ;
 859
 860  {
 861#line 45
 862  excep = (struct __UTAC__EXCEPTION *)exception;
 863#line 46
 864  __cil_tmp5 = (unsigned long )excep;
 865#line 46
 866  __cil_tmp6 = __cil_tmp5 + 24;
 867#line 46
 868  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
 869#line 46
 870  cf = *mem_15;
 871  {
 872#line 49
 873  while (1) {
 874    while_2_continue: /* CIL Label */ ;
 875    {
 876#line 49
 877    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
 878#line 49
 879    __cil_tmp8 = (unsigned long )__cil_tmp7;
 880#line 49
 881    __cil_tmp9 = (unsigned long )cf;
 882#line 49
 883    if (__cil_tmp9 != __cil_tmp8) {
 884
 885    } else {
 886      goto while_2_break;
 887    }
 888    }
 889    {
 890#line 50
 891    tmp = cf;
 892#line 51
 893    __cil_tmp10 = (unsigned long )cf;
 894#line 51
 895    __cil_tmp11 = __cil_tmp10 + 16;
 896#line 51
 897    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
 898#line 51
 899    cf = *mem_16;
 900#line 52
 901    __cil_tmp12 = (void *)tmp;
 902#line 52
 903    free(__cil_tmp12);
 904    }
 905  }
 906  while_2_break: /* CIL Label */ ;
 907  }
 908#line 55
 909  __cil_tmp13 = (unsigned long )excep;
 910#line 55
 911  __cil_tmp14 = __cil_tmp13 + 24;
 912#line 55
 913  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
 914#line 55
 915  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
 916#line 694 "libacc.c"
 917  return;
 918}
 919}
 920#line 59 "libacc.c"
 921void __utac__exception__cf_handler_reset(void *exception ) 
 922{ struct __UTAC__EXCEPTION *excep ;
 923  struct __UTAC__CFLOW_FUNC *cf ;
 924  unsigned long __cil_tmp5 ;
 925  unsigned long __cil_tmp6 ;
 926  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
 927  unsigned long __cil_tmp8 ;
 928  unsigned long __cil_tmp9 ;
 929  int (*__cil_tmp10)(int  , int  ) ;
 930  unsigned long __cil_tmp11 ;
 931  unsigned long __cil_tmp12 ;
 932  int __cil_tmp13 ;
 933  unsigned long __cil_tmp14 ;
 934  unsigned long __cil_tmp15 ;
 935  struct __UTAC__CFLOW_FUNC **mem_16 ;
 936  int (**mem_17)(int  , int  ) ;
 937  int *mem_18 ;
 938  struct __UTAC__CFLOW_FUNC **mem_19 ;
 939
 940  {
 941#line 60
 942  excep = (struct __UTAC__EXCEPTION *)exception;
 943#line 61
 944  __cil_tmp5 = (unsigned long )excep;
 945#line 61
 946  __cil_tmp6 = __cil_tmp5 + 24;
 947#line 61
 948  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
 949#line 61
 950  cf = *mem_16;
 951  {
 952#line 64
 953  while (1) {
 954    while_3_continue: /* CIL Label */ ;
 955    {
 956#line 64
 957    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
 958#line 64
 959    __cil_tmp8 = (unsigned long )__cil_tmp7;
 960#line 64
 961    __cil_tmp9 = (unsigned long )cf;
 962#line 64
 963    if (__cil_tmp9 != __cil_tmp8) {
 964
 965    } else {
 966      goto while_3_break;
 967    }
 968    }
 969    {
 970#line 65
 971    mem_17 = (int (**)(int  , int  ))cf;
 972#line 65
 973    __cil_tmp10 = *mem_17;
 974#line 65
 975    __cil_tmp11 = (unsigned long )cf;
 976#line 65
 977    __cil_tmp12 = __cil_tmp11 + 8;
 978#line 65
 979    mem_18 = (int *)__cil_tmp12;
 980#line 65
 981    __cil_tmp13 = *mem_18;
 982#line 65
 983    (*__cil_tmp10)(4, __cil_tmp13);
 984#line 66
 985    __cil_tmp14 = (unsigned long )cf;
 986#line 66
 987    __cil_tmp15 = __cil_tmp14 + 16;
 988#line 66
 989    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
 990#line 66
 991    cf = *mem_19;
 992    }
 993  }
 994  while_3_break: /* CIL Label */ ;
 995  }
 996  {
 997#line 69
 998  __utac__exception__cf_handler_free(exception);
 999  }
1000#line 732 "libacc.c"
1001  return;
1002}
1003}
1004#line 80 "libacc.c"
1005void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
1006#line 80 "libacc.c"
1007static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
1008#line 79 "libacc.c"
1009void *__utac__error_stack_mgt(void *env , int mode , int count ) 
1010{ void *retValue_acc ;
1011  struct __ACC__ERR *new ;
1012  void *tmp ;
1013  struct __ACC__ERR *temp ;
1014  struct __ACC__ERR *next ;
1015  void *excep ;
1016  unsigned long __cil_tmp10 ;
1017  unsigned long __cil_tmp11 ;
1018  unsigned long __cil_tmp12 ;
1019  unsigned long __cil_tmp13 ;
1020  void *__cil_tmp14 ;
1021  unsigned long __cil_tmp15 ;
1022  unsigned long __cil_tmp16 ;
1023  void *__cil_tmp17 ;
1024  void **mem_18 ;
1025  struct __ACC__ERR **mem_19 ;
1026  struct __ACC__ERR **mem_20 ;
1027  void **mem_21 ;
1028  struct __ACC__ERR **mem_22 ;
1029  void **mem_23 ;
1030  void **mem_24 ;
1031
1032  {
1033#line 82 "libacc.c"
1034  if (count == 0) {
1035#line 758 "libacc.c"
1036    return (retValue_acc);
1037  } else {
1038
1039  }
1040#line 86 "libacc.c"
1041  if (mode == 0) {
1042    {
1043#line 87
1044    tmp = malloc(16UL);
1045#line 87
1046    new = (struct __ACC__ERR *)tmp;
1047#line 88
1048    mem_18 = (void **)new;
1049#line 88
1050    *mem_18 = env;
1051#line 89
1052    __cil_tmp10 = (unsigned long )new;
1053#line 89
1054    __cil_tmp11 = __cil_tmp10 + 8;
1055#line 89
1056    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
1057#line 89
1058    *mem_19 = head;
1059#line 90
1060    head = new;
1061#line 776 "libacc.c"
1062    retValue_acc = (void *)new;
1063    }
1064#line 778
1065    return (retValue_acc);
1066  } else {
1067
1068  }
1069#line 94 "libacc.c"
1070  if (mode == 1) {
1071#line 95
1072    temp = head;
1073    {
1074#line 98
1075    while (1) {
1076      while_4_continue: /* CIL Label */ ;
1077#line 98
1078      if (count > 1) {
1079
1080      } else {
1081        goto while_4_break;
1082      }
1083      {
1084#line 99
1085      __cil_tmp12 = (unsigned long )temp;
1086#line 99
1087      __cil_tmp13 = __cil_tmp12 + 8;
1088#line 99
1089      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
1090#line 99
1091      next = *mem_20;
1092#line 100
1093      mem_21 = (void **)temp;
1094#line 100
1095      excep = *mem_21;
1096#line 101
1097      __cil_tmp14 = (void *)temp;
1098#line 101
1099      free(__cil_tmp14);
1100#line 102
1101      __utac__exception__cf_handler_reset(excep);
1102#line 103
1103      temp = next;
1104#line 104
1105      count = count - 1;
1106      }
1107    }
1108    while_4_break: /* CIL Label */ ;
1109    }
1110    {
1111#line 107
1112    __cil_tmp15 = (unsigned long )temp;
1113#line 107
1114    __cil_tmp16 = __cil_tmp15 + 8;
1115#line 107
1116    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
1117#line 107
1118    head = *mem_22;
1119#line 108
1120    mem_23 = (void **)temp;
1121#line 108
1122    excep = *mem_23;
1123#line 109
1124    __cil_tmp17 = (void *)temp;
1125#line 109
1126    free(__cil_tmp17);
1127#line 110
1128    __utac__exception__cf_handler_reset(excep);
1129#line 820 "libacc.c"
1130    retValue_acc = excep;
1131    }
1132#line 822
1133    return (retValue_acc);
1134  } else {
1135
1136  }
1137#line 114
1138  if (mode == 2) {
1139#line 118 "libacc.c"
1140    if (head) {
1141#line 831
1142      mem_24 = (void **)head;
1143#line 831
1144      retValue_acc = *mem_24;
1145#line 833
1146      return (retValue_acc);
1147    } else {
1148#line 837 "libacc.c"
1149      retValue_acc = (void *)0;
1150#line 839
1151      return (retValue_acc);
1152    }
1153  } else {
1154
1155  }
1156#line 846 "libacc.c"
1157  return (retValue_acc);
1158}
1159}
1160#line 122 "libacc.c"
1161void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
1162{ void *retValue_acc ;
1163  unsigned long __cil_tmp4 ;
1164  unsigned long __cil_tmp5 ;
1165  int __cil_tmp6 ;
1166  int __cil_tmp7 ;
1167  unsigned long __cil_tmp8 ;
1168  unsigned long __cil_tmp9 ;
1169  void **__cil_tmp10 ;
1170  void **__cil_tmp11 ;
1171  int *mem_12 ;
1172  void ***mem_13 ;
1173
1174  {
1175#line 123
1176  if (i > 0) {
1177    {
1178#line 123
1179    __cil_tmp4 = (unsigned long )this;
1180#line 123
1181    __cil_tmp5 = __cil_tmp4 + 16;
1182#line 123
1183    mem_12 = (int *)__cil_tmp5;
1184#line 123
1185    __cil_tmp6 = *mem_12;
1186#line 123
1187    if (i <= __cil_tmp6) {
1188
1189    } else {
1190      {
1191#line 123
1192      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1193                    123U, "__utac__get_this_arg");
1194      }
1195    }
1196    }
1197  } else {
1198    {
1199#line 123
1200    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1201                  123U, "__utac__get_this_arg");
1202    }
1203  }
1204#line 870 "libacc.c"
1205  __cil_tmp7 = i - 1;
1206#line 870
1207  __cil_tmp8 = (unsigned long )this;
1208#line 870
1209  __cil_tmp9 = __cil_tmp8 + 8;
1210#line 870
1211  mem_13 = (void ***)__cil_tmp9;
1212#line 870
1213  __cil_tmp10 = *mem_13;
1214#line 870
1215  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1216#line 870
1217  retValue_acc = *__cil_tmp11;
1218#line 872
1219  return (retValue_acc);
1220#line 879
1221  return (retValue_acc);
1222}
1223}
1224#line 129 "libacc.c"
1225char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
1226{ char const   *retValue_acc ;
1227  unsigned long __cil_tmp4 ;
1228  unsigned long __cil_tmp5 ;
1229  int __cil_tmp6 ;
1230  int __cil_tmp7 ;
1231  unsigned long __cil_tmp8 ;
1232  unsigned long __cil_tmp9 ;
1233  char const   **__cil_tmp10 ;
1234  char const   **__cil_tmp11 ;
1235  int *mem_12 ;
1236  char const   ***mem_13 ;
1237
1238  {
1239#line 131
1240  if (i > 0) {
1241    {
1242#line 131
1243    __cil_tmp4 = (unsigned long )this;
1244#line 131
1245    __cil_tmp5 = __cil_tmp4 + 16;
1246#line 131
1247    mem_12 = (int *)__cil_tmp5;
1248#line 131
1249    __cil_tmp6 = *mem_12;
1250#line 131
1251    if (i <= __cil_tmp6) {
1252
1253    } else {
1254      {
1255#line 131
1256      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1257                    131U, "__utac__get_this_argtype");
1258      }
1259    }
1260    }
1261  } else {
1262    {
1263#line 131
1264    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1265                  131U, "__utac__get_this_argtype");
1266    }
1267  }
1268#line 903 "libacc.c"
1269  __cil_tmp7 = i - 1;
1270#line 903
1271  __cil_tmp8 = (unsigned long )this;
1272#line 903
1273  __cil_tmp9 = __cil_tmp8 + 24;
1274#line 903
1275  mem_13 = (char const   ***)__cil_tmp9;
1276#line 903
1277  __cil_tmp10 = *mem_13;
1278#line 903
1279  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1280#line 903
1281  retValue_acc = *__cil_tmp11;
1282#line 905
1283  return (retValue_acc);
1284#line 912
1285  return (retValue_acc);
1286}
1287}