Showing error 2028

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_product58_safe.cil.c
Line in file: 781
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 751    }
 752  }
 753#line 903 "libacc.c"
 754  __cil_tmp7 = i - 1;
 755#line 903
 756  __cil_tmp8 = (unsigned long )this;
 757#line 903
 758  __cil_tmp9 = __cil_tmp8 + 24;
 759#line 903
 760  mem_13 = (char const   ***)__cil_tmp9;
 761#line 903
 762  __cil_tmp10 = *mem_13;
 763#line 903
 764  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 765#line 903
 766  retValue_acc = *__cil_tmp11;
 767#line 905
 768  return (retValue_acc);
 769#line 912
 770  return (retValue_acc);
 771}
 772}
 773#line 1 "wsllib_check.o"
 774#pragma merger(0,"wsllib_check.i","")
 775#line 3 "wsllib_check.c"
 776void __automaton_fail(void) 
 777{ 
 778
 779  {
 780  goto ERROR;
 781  ERROR: ;
 782#line 53 "wsllib_check.c"
 783  return;
 784}
 785}
 786#line 1 "Environment.o"
 787#pragma merger(0,"Environment.i","")
 788#line 4 "Environment.h"
 789void lowerWaterLevel(void) ;
 790#line 10
 791int isMethaneLevelCritical(void) ;
Show full sources