Showing error 1595

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

Source: 

4290#line 20 "featureselect.c"
4291void select_helpers(void) 
4292{ 
4293
4294  {
4295#line 112 "featureselect.c"
4296  return;
4297}
4298}
4299#line 25 "featureselect.c"
4300int valid_product(void) 
4301{ int retValue_acc ;
4302
4303  {
4304#line 130 "featureselect.c"
4305  retValue_acc = 1;
4306#line 132
4307  return (retValue_acc);
4308#line 139
4309  return (retValue_acc);
4310}
4311}
4312#line 1 "wsllib_check.o"
4313#pragma merger(0,"wsllib_check.i","")
4314#line 3 "wsllib_check.c"
4315void __automaton_fail(void) 
4316{ 
4317
4318  {
4319  goto ERROR;
4320  ERROR: ;
4321#line 53 "wsllib_check.c"
4322  return;
4323}
4324}
4325#line 1 "scenario.o"
4326#pragma merger(0,"scenario.i","")
4327#line 1 "scenario.c"
4328void test(void) 
4329{ 
4330
Show full sources
↑