Showing error 1625

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

Source: 

2374#line 20 "featureselect.c"
2375void select_helpers(void) 
2376{ 
2377
2378  {
2379#line 112 "featureselect.c"
2380  return;
2381}
2382}
2383#line 25 "featureselect.c"
2384int valid_product(void) 
2385{ int retValue_acc ;
2386
2387  {
2388#line 130 "featureselect.c"
2389  retValue_acc = 1;
2390#line 132
2391  return (retValue_acc);
2392#line 139
2393  return (retValue_acc);
2394}
2395}
2396#line 1 "wsllib_check.o"
2397#pragma merger(0,"wsllib_check.i","")
2398#line 3 "wsllib_check.c"
2399void __automaton_fail(void) 
2400{ 
2401
2402  {
2403  goto ERROR;
2404  ERROR: ;
2405#line 53 "wsllib_check.c"
2406  return;
2407}
2408}
2409#line 1 "Floor.o"
2410#pragma merger(0,"Floor.i","")
2411#line 16 "Floor.h"
2412void callOnFloor(int floorID ) ;
2413#line 20
2414void initPersonOnFloor(int person , int floor ) ;
Show full sources
↑