Showing error 2144

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

Source: 

1271#line 85
1272  tmp = valid_product();
1273  }
1274#line 85
1275  if (tmp) {
1276    {
1277#line 86
1278    setup();
1279#line 87
1280    runTest();
1281    }
1282  } else {
1283
1284  }
1285#line 1234 "Test.c"
1286  retValue_acc = 0;
1287#line 1236
1288  return (retValue_acc);
1289#line 1243
1290  return (retValue_acc);
1291}
1292}
1293#line 1 "wsllib_check.o"
1294#pragma merger(0,"wsllib_check.i","")
1295#line 3 "wsllib_check.c"
1296void __automaton_fail(void) 
1297{ 
1298
1299  {
1300  goto ERROR;
1301  ERROR: ;
1302#line 53 "wsllib_check.c"
1303  return;
1304}
1305}
1306#line 1 "Specification5_spec.o"
1307#pragma merger(0,"Specification5_spec.i","")
1308#line 7 "Specification5_spec.c"
1309int switchedOnBeforeTS  ;
1310#line 11 "Specification5_spec.c"
1311void __utac_acc__Specification5_spec__1(void)
Show full sources
↑