Showing error 1617

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

Source: 

2534#line 2583 "Elevator.c"
2535  retValue_acc = isFloorCalling(executiveFloor);
2536  }
2537#line 2585
2538  return (retValue_acc);
2539#line 2592
2540  return (retValue_acc);
2541}
2542}
2543#line 443 "Elevator.c"
2544int isExecutiveFloor(int floorID ) 
2545{ int retValue_acc ;
2546
2547  {
2548#line 2614 "Elevator.c"
2549  retValue_acc = executiveFloor == floorID;
2550#line 2616
2551  return (retValue_acc);
2552#line 2623
2553  return (retValue_acc);
2554}
2555}
2556#line 1 "wsllib_check.o"
2557#pragma merger(0,"wsllib_check.i","")
2558#line 3 "wsllib_check.c"
2559void __automaton_fail(void) 
2560{ 
2561
2562  {
2563  goto ERROR;
2564  ERROR: ;
2565#line 53 "wsllib_check.c"
2566  return;
2567}
2568}
2569#line 1 "libacc.o"
2570#pragma merger(0,"libacc.i","")
2571#line 73 "/usr/include/assert.h"
2572extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
2573                                                                      char const   *__file ,
2574                                                                      unsigned int __line ,
Show full sources
↑