Showing error 1590

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

Source: 

4077
4078      } else {
4079        goto while_6_break;
4080      }
4081    } else {
4082      goto while_6_break;
4083    }
4084    {
4085#line 58
4086    timeShift();
4087#line 59
4088    printState();
4089#line 57
4090    i = i + 1;
4091    }
4092  }
4093  while_6_break: /* CIL Label */ ;
4094  }
4095#line 1117 "UnitTests.c"
4096  return;
4097}
4098}
4099#line 1 "wsllib_check.o"
4100#pragma merger(0,"wsllib_check.i","")
4101#line 3 "wsllib_check.c"
4102void __automaton_fail(void) 
4103{ 
4104
4105  {
4106  goto ERROR;
4107  ERROR: ;
4108#line 53 "wsllib_check.c"
4109  return;
4110}
4111}
4112#line 1 "scenario.o"
4113#pragma merger(0,"scenario.i","")
4114#line 1 "scenario.c"
4115void test(void) 
4116{ 
4117
Show full sources
↑