Showing error 1621

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

Source: 

4405#line 20 "featureselect.c"
4406void select_helpers(void) 
4407{ 
4408
4409  {
4410#line 112 "featureselect.c"
4411  return;
4412}
4413}
4414#line 25 "featureselect.c"
4415int valid_product(void) 
4416{ int retValue_acc ;
4417
4418  {
4419#line 130 "featureselect.c"
4420  retValue_acc = 1;
4421#line 132
4422  return (retValue_acc);
4423#line 139
4424  return (retValue_acc);
4425}
4426}
4427#line 1 "wsllib_check.o"
4428#pragma merger(0,"wsllib_check.i","")
4429#line 3 "wsllib_check.c"
4430void __automaton_fail(void) 
4431{ 
4432
4433  {
4434  goto ERROR;
4435  ERROR: ;
4436#line 53 "wsllib_check.c"
4437  return;
4438}
4439}
4440#line 1 "UnitTests.o"
4441#pragma merger(0,"UnitTests.i","")
4442#line 24 "UnitTests.c"
4443void spec1(void) 
4444{ int tmp ;
4445  int tmp___0 ;
Show full sources
↑