Showing error 1971

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