Showing error 1654

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

Source: 

1636#line 176
1637  tmp = valid_product();
1638  }
1639#line 176
1640  if (tmp) {
1641    {
1642#line 177
1643    setup();
1644#line 178
1645    runTest();
1646    }
1647  } else {
1648
1649  }
1650#line 1620 "Test.c"
1651  retValue_acc = 0;
1652#line 1622
1653  return (retValue_acc);
1654#line 1629
1655  return (retValue_acc);
1656}
1657}
1658#line 1 "wsllib_check.o"
1659#pragma merger(0,"wsllib_check.i","")
1660#line 3 "wsllib_check.c"
1661void __automaton_fail(void) 
1662{ 
1663
1664  {
1665  goto ERROR;
1666  ERROR: ;
1667#line 53 "wsllib_check.c"
1668  return;
1669}
1670}
1671#line 1 "Floor.o"
1672#pragma merger(0,"Floor.i","")
1673#line 12 "Floor.h"
1674int isFloorCalling(int floorID ) ;
1675#line 14
1676void resetCallOnFloor(int floorID ) ;
Show full sources
↑