Showing error 2002

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

Source: 

 964    deactivatePump();
 965    }
 966  } else {
 967
 968  }
 969#line 89
 970  systemActive = 0;
 971#line 395 "MinePump.c"
 972  return;
 973}
 974}
 975#line 91 "MinePump.c"
 976void startSystem(void) 
 977{ 
 978
 979  {
 980#line 93
 981  systemActive = 1;
 982#line 415 "MinePump.c"
 983  return;
 984}
 985}
 986#line 1 "wsllib_check.o"
 987#pragma merger(0,"wsllib_check.i","")
 988#line 3 "wsllib_check.c"
 989void __automaton_fail(void) 
 990{ 
 991
 992  {
 993  goto ERROR;
 994  ERROR: ;
 995#line 53 "wsllib_check.c"
 996  return;
 997}
 998}
 999#line 1 "Test.o"
1000#pragma merger(0,"Test.i","")
1001#line 8 "Test.c"
1002int cleanupTimeShifts  =    4;
1003#line 11 "Test.c"
1004#line 17 "Test.c"
Show full sources
↑