Showing error 1637

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

Source: 

3750    if (expectedDirection == 1) {
3751      {
3752#line 40
3753      tmp = getCurrentHeading();
3754      }
3755#line 40
3756      if (tmp == 0) {
3757        {
3758#line 41
3759        __automaton_fail();
3760        }
3761      } else {
3762
3763      }
3764    } else {
3765
3766    }
3767  }
3768#line 41
3769  return;
3770}
3771}
3772#line 1 "wsllib_check.o"
3773#pragma merger(0,"wsllib_check.i","")
3774#line 3 "wsllib_check.c"
3775void __automaton_fail(void) 
3776{ 
3777
3778  {
3779  goto ERROR;
3780  ERROR: ;
3781#line 53 "wsllib_check.c"
3782  return;
3783}
3784}
3785#line 1 "UnitTests.o"
3786#pragma merger(0,"UnitTests.i","")
3787#line 24 "UnitTests.c"
3788void spec1(void) 
3789{ int tmp ;
3790  int tmp___0 ;
Show full sources
↑