Showing error 1653

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

Source: 

4870  }
4871  {
4872#line 265
4873  resetCallOnFloor(floor);
4874  }
4875#line 1694 "Floor.c"
4876  return;
4877}
4878}
4879#line 268 "Floor.c"
4880int isTopFloor(int floorID ) 
4881{ int retValue_acc ;
4882
4883  {
4884#line 1712 "Floor.c"
4885  retValue_acc = floorID == 4;
4886#line 1714
4887  return (retValue_acc);
4888#line 1721
4889  return (retValue_acc);
4890}
4891}
4892#line 1 "wsllib_check.o"
4893#pragma merger(0,"wsllib_check.i","")
4894#line 3 "wsllib_check.c"
4895void __automaton_fail(void) 
4896{ 
4897
4898  {
4899  goto ERROR;
4900  ERROR: ;
4901#line 53 "wsllib_check.c"
4902  return;
4903}
4904}
Show full sources
↑