Showing error 1970

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

Source: 

1406    if (tmp___0 == 2) {
1407      {
1408#line 19
1409      tmp___1 = isPumpRunning();
1410      }
1411#line 19
1412      if (tmp___1) {
1413
1414      } else {
1415        {
1416#line 16
1417        __automaton_fail();
1418        }
1419      }
1420    } else {
1421
1422    }
1423  }
1424#line 16
1425  return;
1426}
1427}
1428#line 1 "wsllib_check.o"
1429#pragma merger(0,"wsllib_check.i","")
1430#line 3 "wsllib_check.c"
1431void __automaton_fail(void) 
1432{ 
1433
1434  {
1435  goto ERROR;
1436  ERROR: ;
1437#line 53 "wsllib_check.c"
1438  return;
1439}
1440}
1441#line 1 "Environment.o"
1442#pragma merger(0,"Environment.i","")
1443#line 9 "Environment.c"
1444int waterLevel  =    1;
1445#line 12 "Environment.c"
1446int methaneLevelCritical  =    0;
Show full sources
↑