Showing error 1661

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_spec9_product32_unsafe.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 "scenario.o"
1086#pragma merger(0,"scenario.i","")
1087#line 2 "scenario.c"
1088void bigMacCall(void) ;
1089#line 3
1090void cleanup(void) ;
Show full sources
↑