Showing error 1858

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


Source:

1110    }
1111  }
1112#line 903 "libacc.c"
1113  __cil_tmp7 = i - 1;
1114#line 903
1115  __cil_tmp8 = (unsigned long )this;
1116#line 903
1117  __cil_tmp9 = __cil_tmp8 + 24;
1118#line 903
1119  mem_13 = (char const   ***)__cil_tmp9;
1120#line 903
1121  __cil_tmp10 = *mem_13;
1122#line 903
1123  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1124#line 903
1125  retValue_acc = *__cil_tmp11;
1126#line 905
1127  return (retValue_acc);
1128#line 912
1129  return (retValue_acc);
1130}
1131}
1132#line 1 "wsllib_check.o"
1133#pragma merger(0,"wsllib_check.i","")
1134#line 3 "wsllib_check.c"
1135void __automaton_fail(void) 
1136{ 
1137
1138  {
1139  goto ERROR;
1140  ERROR: ;
1141#line 53 "wsllib_check.c"
1142  return;
1143}
1144}
1145#line 1 "Environment.o"
1146#pragma merger(0,"Environment.i","")
1147#line 12 "Environment.h"
1148int getWaterLevel(void) ;
1149#line 9 "Environment.c"
1150int waterLevel  =    1;
Show full sources