Showing error 1616

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


Source:

2223#line 2530 "Elevator.c"
2224  retValue_acc = isFloorCalling(executiveFloor);
2225  }
2226#line 2532
2227  return (retValue_acc);
2228#line 2539
2229  return (retValue_acc);
2230}
2231}
2232#line 429 "Elevator.c"
2233int isExecutiveFloor(int floorID ) 
2234{ int retValue_acc ;
2235
2236  {
2237#line 2561 "Elevator.c"
2238  retValue_acc = executiveFloor == floorID;
2239#line 2563
2240  return (retValue_acc);
2241#line 2570
2242  return (retValue_acc);
2243}
2244}
2245#line 1 "wsllib_check.o"
2246#pragma merger(0,"wsllib_check.i","")
2247#line 3 "wsllib_check.c"
2248void __automaton_fail(void) 
2249{ 
2250
2251  {
2252  goto ERROR;
2253  ERROR: ;
2254#line 53 "wsllib_check.c"
2255  return;
2256}
2257}
2258#line 1 "Floor.o"
2259#pragma merger(0,"Floor.i","")
2260#line 16 "Floor.h"
2261void callOnFloor(int floorID ) ;
2262#line 20
2263void initPersonOnFloor(int person , int floor ) ;
Show full sources