Showing error 2066

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

Source: 

1305#line 17
1306  if (tmp == 0) {
1307    {
1308#line 17
1309    tmp___0 = isPumpRunning();
1310    }
1311#line 17
1312    if (tmp___0) {
1313      {
1314#line 14
1315      __automaton_fail();
1316      }
1317    } else {
1318
1319    }
1320  } else {
1321
1322  }
1323#line 14
1324  return;
1325}
1326}
1327#line 1 "wsllib_check.o"
1328#pragma merger(0,"wsllib_check.i","")
1329#line 3 "wsllib_check.c"
1330void __automaton_fail(void) 
1331{ 
1332
1333  {
1334  goto ERROR;
1335  ERROR: ;
1336#line 53 "wsllib_check.c"
1337  return;
1338}
1339}
Show full sources
↑