Showing error 1576

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

Source: 

2887#line 20 "featureselect.c"
2888void select_helpers(void) 
2889{ 
2890
2891  {
2892#line 112 "featureselect.c"
2893  return;
2894}
2895}
2896#line 25 "featureselect.c"
2897int valid_product(void) 
2898{ int retValue_acc ;
2899
2900  {
2901#line 130 "featureselect.c"
2902  retValue_acc = 1;
2903#line 132
2904  return (retValue_acc);
2905#line 139
2906  return (retValue_acc);
2907}
2908}
2909#line 1 "wsllib_check.o"
2910#pragma merger(0,"wsllib_check.i","")
2911#line 3 "wsllib_check.c"
2912void __automaton_fail(void) 
2913{ 
2914
2915  {
2916  goto ERROR;
2917  ERROR: ;
2918#line 53 "wsllib_check.c"
2919  return;
2920}
2921}
2922#line 1 "UnitTests.o"
2923#pragma merger(0,"UnitTests.i","")
2924#line 12 "Person.h"
2925int getOrigin(int person ) ;
2926#line 20 "Floor.h"
2927void initPersonOnFloor(int person , int floor ) ;
Show full sources
↑