Showing error 1599

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

Source: 

4659#line 2473 "Elevator.c"
4660  retValue_acc = isFloorCalling(executiveFloor);
4661  }
4662#line 2475
4663  return (retValue_acc);
4664#line 2482
4665  return (retValue_acc);
4666}
4667}
4668#line 419 "Elevator.c"
4669int isExecutiveFloor(int floorID ) 
4670{ int retValue_acc ;
4671
4672  {
4673#line 2504 "Elevator.c"
4674  retValue_acc = executiveFloor == floorID;
4675#line 2506
4676  return (retValue_acc);
4677#line 2513
4678  return (retValue_acc);
4679}
4680}
4681#line 1 "wsllib_check.o"
4682#pragma merger(0,"wsllib_check.i","")
4683#line 3 "wsllib_check.c"
4684void __automaton_fail(void) 
4685{ 
4686
4687  {
4688  goto ERROR;
4689  ERROR: ;
4690#line 53 "wsllib_check.c"
4691  return;
4692}
4693}
Show full sources
↑