Showing error 1932

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

Source: 

1293}
1294}
1295#line 77 "MinePump.c"
1296void stopSystem(void) 
1297{ 
1298
1299  {
1300#line 82
1301  if (pumpRunning) {
1302    {
1303#line 79
1304    deactivatePump();
1305    }
1306  } else {
1307
1308  }
1309#line 82
1310  systemActive = 0;
1311#line 367 "MinePump.c"
1312  return;
1313}
1314}
1315#line 1 "wsllib_check.o"
1316#pragma merger(0,"wsllib_check.i","")
1317#line 3 "wsllib_check.c"
1318void __automaton_fail(void) 
1319{ 
1320
1321  {
1322  goto ERROR;
1323  ERROR: ;
1324#line 53 "wsllib_check.c"
1325  return;
1326}
1327}
Show full sources
↑