Showing error 1888

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

Source: 

1189    deactivatePump();
1190    }
1191  } else {
1192
1193  }
1194#line 89
1195  systemActive = 0;
1196#line 395 "MinePump.c"
1197  return;
1198}
1199}
1200#line 91 "MinePump.c"
1201void startSystem(void) 
1202{ 
1203
1204  {
1205#line 93
1206  systemActive = 1;
1207#line 415 "MinePump.c"
1208  return;
1209}
1210}
1211#line 1 "wsllib_check.o"
1212#pragma merger(0,"wsllib_check.i","")
1213#line 3 "wsllib_check.c"
1214void __automaton_fail(void) 
1215{ 
1216
1217  {
1218  goto ERROR;
1219  ERROR: ;
1220#line 53 "wsllib_check.c"
1221  return;
1222}
1223}
1224#line 1 "scenario.o"
1225#pragma merger(0,"scenario.i","")
1226#line 1 "scenario.c"
1227void test(void) 
1228{ int splverifierCounter ;
1229  int tmp ;
Show full sources
↑