Showing error 1604

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

Source: 

4851
4852      } else {
4853        goto while_9_break;
4854      }
4855    } else {
4856      goto while_9_break;
4857    }
4858    {
4859#line 58
4860    timeShift();
4861#line 59
4862    printState();
4863#line 57
4864    i = i + 1;
4865    }
4866  }
4867  while_9_break: /* CIL Label */ ;
4868  }
4869#line 1125 "UnitTests.c"
4870  return;
4871}
4872}
4873#line 1 "wsllib_check.o"
4874#pragma merger(0,"wsllib_check.i","")
4875#line 3 "wsllib_check.c"
4876void __automaton_fail(void) 
4877{ 
4878
4879  {
4880  goto ERROR;
4881  ERROR: ;
4882#line 53 "wsllib_check.c"
4883  return;
4884}
4885}
Show full sources
↑