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_product54_safe.cil.c |
Line in file: | 1412 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1382#line 20 "featureselect.c" 1383void select_helpers(void) 1384{ 1385 1386 { 1387#line 111 "featureselect.c" 1388 return; 1389} 1390} 1391#line 25 "featureselect.c" 1392int valid_product(void) 1393{ int retValue_acc ; 1394 1395 { 1396#line 129 "featureselect.c" 1397 retValue_acc = 1; 1398#line 131 1399 return (retValue_acc); 1400#line 138 1401 return (retValue_acc); 1402} 1403} 1404#line 1 "wsllib_check.o" 1405#pragma merger(0,"wsllib_check.i","") 1406#line 3 "wsllib_check.c" 1407void __automaton_fail(void) 1408{ 1409 1410 { 1411 goto ERROR; 1412 ERROR: ; 1413#line 53 "wsllib_check.c" 1414 return; 1415} 1416}