Showing error 1627

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


Source:

 865
 866      } else {
 867        goto while_3_break;
 868      }
 869    } else {
 870      goto while_3_break;
 871    }
 872    {
 873#line 58
 874    timeShift();
 875#line 59
 876    printState();
 877#line 57
 878    i = i + 1;
 879    }
 880  }
 881  while_3_break: /* CIL Label */ ;
 882  }
 883#line 1119 "UnitTests.c"
 884  return;
 885}
 886}
 887#line 1 "wsllib_check.o"
 888#pragma merger(0,"wsllib_check.i","")
 889#line 3 "wsllib_check.c"
 890void __automaton_fail(void) 
 891{ 
 892
 893  {
 894  goto ERROR;
 895  ERROR: ;
 896#line 53 "wsllib_check.c"
 897  return;
 898}
 899}
 900#line 1 "Floor.o"
 901#pragma merger(0,"Floor.i","")
 902#line 12 "Floor.h"
 903int isFloorCalling(int floorID ) ;
 904#line 14
 905void resetCallOnFloor(int floorID ) ;
Show full sources