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_spec3_productSimulator_unsafe.cil.c |
Line in file: | 1772 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1742 1743 } else { 1744 goto while_4_break; 1745 } 1746 } else { 1747 goto while_4_break; 1748 } 1749 { 1750#line 58 1751 timeShift(); 1752#line 59 1753 printState(); 1754#line 57 1755 i = i + 1; 1756 } 1757 } 1758 while_4_break: /* CIL Label */ ; 1759 } 1760#line 1138 "UnitTests.c" 1761 return; 1762} 1763} 1764#line 1 "wsllib_check.o" 1765#pragma merger(0,"wsllib_check.i","") 1766#line 3 "wsllib_check.c" 1767void __automaton_fail(void) 1768{ 1769 1770 { 1771 goto ERROR; 1772 ERROR: ; 1773#line 53 "wsllib_check.c" 1774 return; 1775} 1776} 1777#line 1 "Elevator.o" 1778#pragma merger(0,"Elevator.i","") 1779#line 359 "/usr/include/stdio.h" 1780extern int printf(char const * __restrict __format , ...) ; 1781#line 10 "Person.h" 1782int getWeight(int person ) ;