Showing error 1935

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

Source: 

1264#line 355
1265    tmp___0 = 1;
1266  }
1267#line 355
1268  retValue_acc = tmp___0;
1269#line 357
1270  return (retValue_acc);
1271#line 364
1272  return (retValue_acc);
1273}
1274}
1275#line 84 "MinePump.c"
1276void startSystem(void) 
1277{ 
1278
1279  {
1280#line 86
1281  systemActive = 1;
1282#line 388 "MinePump.c"
1283  return;
1284}
1285}
1286#line 1 "wsllib_check.o"
1287#pragma merger(0,"wsllib_check.i","")
1288#line 3 "wsllib_check.c"
1289void __automaton_fail(void) 
1290{ 
1291
1292  {
1293  goto ERROR;
1294  ERROR: ;
1295#line 53 "wsllib_check.c"
1296  return;
1297}
1298}
1299#line 1 "Specification2_spec.o"
1300#pragma merger(0,"Specification2_spec.i","")
1301#line 7 "Specification2_spec.c"
1302int methAndRunningLastTime  ;
1303#line 11 "Specification2_spec.c"
1304void __utac_acc__Specification2_spec__1(void)
Show full sources
↑