Showing error 1644

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

Source: 

4584          } else {
4585#line 1188
4586            if (person == 5) {
4587#line 1193
4588              retValue_acc = 3;
4589#line 1195
4590              return (retValue_acc);
4591            } else {
4592#line 1201 "Person.c"
4593              retValue_acc = 0;
4594#line 1203
4595              return (retValue_acc);
4596            }
4597          }
4598        }
4599      }
4600    }
4601  }
4602#line 1210 "Person.c"
4603  return (retValue_acc);
4604}
4605}
4606#line 1 "wsllib_check.o"
4607#pragma merger(0,"wsllib_check.i","")
4608#line 3 "wsllib_check.c"
4609void __automaton_fail(void) 
4610{ 
4611
4612  {
4613  goto ERROR;
4614  ERROR: ;
4615#line 53 "wsllib_check.c"
4616  return;
4617}
4618}
4619#line 1 "featureselect.o"
4620#pragma merger(0,"featureselect.i","")
4621#line 9 "featureselect.h"
4622int select_one(void) ;
4623#line 8 "featureselect.c"
4624int select_one(void)
Show full sources
↑