Showing error 1614

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

Source: 

1050  }
1051  {
1052#line 265
1053  resetCallOnFloor(floor);
1054  }
1055#line 1694 "Floor.c"
1056  return;
1057}
1058}
1059#line 268 "Floor.c"
1060int isTopFloor(int floorID ) 
1061{ int retValue_acc ;
1062
1063  {
1064#line 1712 "Floor.c"
1065  retValue_acc = floorID == 4;
1066#line 1714
1067  return (retValue_acc);
1068#line 1721
1069  return (retValue_acc);
1070}
1071}
1072#line 1 "wsllib_check.o"
1073#pragma merger(0,"wsllib_check.i","")
1074#line 3 "wsllib_check.c"
1075void __automaton_fail(void) 
1076{ 
1077
1078  {
1079  goto ERROR;
1080  ERROR: ;
1081#line 53 "wsllib_check.c"
1082  return;
1083}
1084}
1085#line 1 "Person.o"
1086#pragma merger(0,"Person.i","")
1087#line 10 "Person.h"
1088int getWeight(int person ) ;
1089#line 12
1090int getOrigin(int person ) ;
Show full sources
↑