Showing error 2047

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


Source:

1210    }
1211  }
1212#line 903 "libacc.c"
1213  __cil_tmp7 = i - 1;
1214#line 903
1215  __cil_tmp8 = (unsigned long )this;
1216#line 903
1217  __cil_tmp9 = __cil_tmp8 + 24;
1218#line 903
1219  mem_13 = (char const   ***)__cil_tmp9;
1220#line 903
1221  __cil_tmp10 = *mem_13;
1222#line 903
1223  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1224#line 903
1225  retValue_acc = *__cil_tmp11;
1226#line 905
1227  return (retValue_acc);
1228#line 912
1229  return (retValue_acc);
1230}
1231}
1232#line 1 "wsllib_check.o"
1233#pragma merger(0,"wsllib_check.i","")
1234#line 3 "wsllib_check.c"
1235void __automaton_fail(void) 
1236{ 
1237
1238  {
1239  goto ERROR;
1240  ERROR: ;
1241#line 53 "wsllib_check.c"
1242  return;
1243}
1244}
Show full sources