Showing error 1983

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