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/elevator_spec13_product29_safe.cil.c |
Line in file: | 3611 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
3581#line 30 3582 __automaton_fail(); 3583 } 3584 } else { 3585 3586 } 3587 } 3588 } else { 3589 3590 } 3591 } else { 3592 3593 } 3594 } 3595 } else { 3596 3597 } 3598 } 3599#line 30 3600 return; 3601} 3602} 3603#line 1 "wsllib_check.o" 3604#pragma merger(0,"wsllib_check.i","") 3605#line 3 "wsllib_check.c" 3606void __automaton_fail(void) 3607{ 3608 3609 { 3610 goto ERROR; 3611 ERROR: ; 3612#line 53 "wsllib_check.c" 3613 return; 3614} 3615} 3616#line 1 "UnitTests.o" 3617#pragma merger(0,"UnitTests.i","") 3618#line 13 "UnitTests.c" 3619int cleanupTimeShifts = 12; 3620#line 24 "UnitTests.c" 3621void spec1(void)