Showing error 1573

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

Source: 

1609void bigMacCall(void) ;
1610#line 3
1611void angelinaCall(void) ;
1612#line 4
1613void cleanup(void) ;
1614#line 1 "scenario.c"
1615void test(void) 
1616{ 
1617
1618  {
1619  {
1620#line 2
1621  bigMacCall();
1622#line 3
1623  angelinaCall();
1624#line 4
1625  cleanup();
1626  }
1627#line 55 "scenario.c"
1628  return;
1629}
1630}
1631#line 1 "wsllib_check.o"
1632#pragma merger(0,"wsllib_check.i","")
1633#line 3 "wsllib_check.c"
1634void __automaton_fail(void) 
1635{ 
1636
1637  {
1638  goto ERROR;
1639  ERROR: ;
1640#line 53 "wsllib_check.c"
1641  return;
1642}
1643}
1644#line 1 "featureselect.o"
1645#pragma merger(0,"featureselect.i","")
1646#line 9 "featureselect.h"
1647int select_one(void) ;
1648#line 11
1649void select_features(void) ;
Show full sources
↑