Showing error 1955

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


Source:

1347    }
1348  }
1349#line 903 "libacc.c"
1350  __cil_tmp7 = i - 1;
1351#line 903
1352  __cil_tmp8 = (unsigned long )this;
1353#line 903
1354  __cil_tmp9 = __cil_tmp8 + 24;
1355#line 903
1356  mem_13 = (char const   ***)__cil_tmp9;
1357#line 903
1358  __cil_tmp10 = *mem_13;
1359#line 903
1360  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1361#line 903
1362  retValue_acc = *__cil_tmp11;
1363#line 905
1364  return (retValue_acc);
1365#line 912
1366  return (retValue_acc);
1367}
1368}
1369#line 1 "wsllib_check.o"
1370#pragma merger(0,"wsllib_check.i","")
1371#line 3 "wsllib_check.c"
1372void __automaton_fail(void) 
1373{ 
1374
1375  {
1376  goto ERROR;
1377  ERROR: ;
1378#line 53 "wsllib_check.c"
1379  return;
1380}
1381}
Show full sources