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_product62_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 17 1383 if (tmp) { 1384 { 1385#line 17 1386 tmp___0 = isPumpRunning(); 1387 } 1388#line 17 1389 if (tmp___0) { 1390 { 1391#line 14 1392 __automaton_fail(); 1393 } 1394 } else { 1395 1396 } 1397 } else { 1398 1399 } 1400#line 14 1401 return; 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}