Showing error 1842

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