Showing error 1594

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


Source:

3581#line 30
3582              __automaton_fail();
3583              }
3584            } else {
3585
3586            }
3587          }
3588        } else {
3589
3590        }
3591      } else {
3592
3593      }
3594    }
3595  } else {
3596
3597  }
3598  }
3599#line 30
3600  return;
3601}
3602}
3603#line 1 "wsllib_check.o"
3604#pragma merger(0,"wsllib_check.i","")
3605#line 3 "wsllib_check.c"
3606void __automaton_fail(void) 
3607{ 
3608
3609  {
3610  goto ERROR;
3611  ERROR: ;
3612#line 53 "wsllib_check.c"
3613  return;
3614}
3615}
3616#line 1 "UnitTests.o"
3617#pragma merger(0,"UnitTests.i","")
3618#line 13 "UnitTests.c"
3619int cleanupTimeShifts  =    12;
3620#line 24 "UnitTests.c"
3621void spec1(void) 
Show full sources