Showing error 2105

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


Source:

 908    }
 909  }
 910#line 903 "libacc.c"
 911  __cil_tmp7 = i - 1;
 912#line 903
 913  __cil_tmp8 = (unsigned long )this;
 914#line 903
 915  __cil_tmp9 = __cil_tmp8 + 24;
 916#line 903
 917  mem_13 = (char const   ***)__cil_tmp9;
 918#line 903
 919  __cil_tmp10 = *mem_13;
 920#line 903
 921  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
 922#line 903
 923  retValue_acc = *__cil_tmp11;
 924#line 905
 925  return (retValue_acc);
 926#line 912
 927  return (retValue_acc);
 928}
 929}
 930#line 1 "wsllib_check.o"
 931#pragma merger(0,"wsllib_check.i","")
 932#line 3 "wsllib_check.c"
 933void __automaton_fail(void) 
 934{ 
 935
 936  {
 937  goto ERROR;
 938  ERROR: ;
 939#line 53 "wsllib_check.c"
 940  return;
 941}
 942}
 943#line 1 "Test.o"
 944#pragma merger(0,"Test.i","")
 945#line 8 "Test.c"
 946int cleanupTimeShifts  =    4;
 947#line 11 "Test.c"
 948#line 17 "Test.c"
Show full sources