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_product64_unsafe.cil.c |
Line in file: | 1401 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1371#line 85 1372 tmp = valid_product(); 1373 } 1374#line 85 1375 if (tmp) { 1376 { 1377#line 86 1378 setup(); 1379#line 87 1380 runTest(); 1381 } 1382 } else { 1383 1384 } 1385#line 1226 "Test.c" 1386 retValue_acc = 0; 1387#line 1228 1388 return (retValue_acc); 1389#line 1235 1390 return (retValue_acc); 1391} 1392} 1393#line 1 "wsllib_check.o" 1394#pragma merger(0,"wsllib_check.i","") 1395#line 3 "wsllib_check.c" 1396void __automaton_fail(void) 1397{ 1398 1399 { 1400 goto ERROR; 1401 ERROR: ; 1402#line 53 "wsllib_check.c" 1403 return; 1404} 1405} 1406#line 1 "Specification3_spec.o" 1407#pragma merger(0,"Specification3_spec.i","") 1408#line 11 "Specification3_spec.c" 1409void __utac_acc__Specification3_spec__1(void) 1410{ int tmp ; 1411 int tmp___0 ;