Showing error 1578

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_spec1_product22_unsafe.cil.c
Line in file: 1614
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

1584  }
1585  {
1586#line 265
1587  resetCallOnFloor(floor);
1588  }
1589#line 1703 "Floor.c"
1590  return;
1591}
1592}
1593#line 268 "Floor.c"
1594int isTopFloor(int floorID ) 
1595{ int retValue_acc ;
1596
1597  {
1598#line 1721 "Floor.c"
1599  retValue_acc = floorID == 4;
1600#line 1723
1601  return (retValue_acc);
1602#line 1730
1603  return (retValue_acc);
1604}
1605}
1606#line 1 "wsllib_check.o"
1607#pragma merger(0,"wsllib_check.i","")
1608#line 3 "wsllib_check.c"
1609void __automaton_fail(void) 
1610{ 
1611
1612  {
1613  goto ERROR;
1614  ERROR: ;
1615#line 53 "wsllib_check.c"
1616  return;
1617}
1618}
1619#line 1 "UnitTests.o"
1620#pragma merger(0,"UnitTests.i","")
1621#line 12 "Person.h"
1622int getOrigin(int person ) ;
1623#line 20 "Elevator.h"
1624void timeShift(void) ;
Show full sources
↑