Showing error 1572

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

Source: 

2721#line 20 "featureselect.c"
2722void select_helpers(void) 
2723{ 
2724
2725  {
2726#line 112 "featureselect.c"
2727  return;
2728}
2729}
2730#line 25 "featureselect.c"
2731int valid_product(void) 
2732{ int retValue_acc ;
2733
2734  {
2735#line 130 "featureselect.c"
2736  retValue_acc = 1;
2737#line 132
2738  return (retValue_acc);
2739#line 139
2740  return (retValue_acc);
2741}
2742}
2743#line 1 "wsllib_check.o"
2744#pragma merger(0,"wsllib_check.i","")
2745#line 3 "wsllib_check.c"
2746void __automaton_fail(void) 
2747{ 
2748
2749  {
2750  goto ERROR;
2751  ERROR: ;
2752#line 53 "wsllib_check.c"
2753  return;
2754}
2755}
2756#line 1 "UnitTests.o"
2757#pragma merger(0,"UnitTests.i","")
2758#line 20 "Floor.h"
2759void initPersonOnFloor(int person , int floor ) ;
2760#line 13 "UnitTests.c"
2761int cleanupTimeShifts  =    12;
Show full sources
↑