Showing error 1584

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

Source: 

4454#line 2607 "Elevator.c"
4455  retValue_acc = isFloorCalling(executiveFloor);
4456  }
4457#line 2609
4458  return (retValue_acc);
4459#line 2616
4460  return (retValue_acc);
4461}
4462}
4463#line 454 "Elevator.c"
4464int isExecutiveFloor(int floorID ) 
4465{ int retValue_acc ;
4466
4467  {
4468#line 2638 "Elevator.c"
4469  retValue_acc = executiveFloor == floorID;
4470#line 2640
4471  return (retValue_acc);
4472#line 2647
4473  return (retValue_acc);
4474}
4475}
4476#line 1 "wsllib_check.o"
4477#pragma merger(0,"wsllib_check.i","")
4478#line 3 "wsllib_check.c"
4479void __automaton_fail(void) 
4480{ 
4481
4482  {
4483  goto ERROR;
4484  ERROR: ;
4485#line 53 "wsllib_check.c"
4486  return;
4487}
4488}
4489#line 1 "scenario.o"
4490#pragma merger(0,"scenario.i","")
4491#line 1 "scenario.c"
4492void test(void) 
4493{ 
4494
Show full sources
↑