Showing error 1657

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

Source: 

4974
4975      } else {
4976        goto while_9_break;
4977      }
4978    } else {
4979      goto while_9_break;
4980    }
4981    {
4982#line 58
4983    timeShift();
4984#line 59
4985    printState();
4986#line 57
4987    i = i + 1;
4988    }
4989  }
4990  while_9_break: /* CIL Label */ ;
4991  }
4992#line 1125 "UnitTests.c"
4993  return;
4994}
4995}
4996#line 1 "wsllib_check.o"
4997#pragma merger(0,"wsllib_check.i","")
4998#line 3 "wsllib_check.c"
4999void __automaton_fail(void) 
5000{ 
5001
5002  {
5003  goto ERROR;
5004  ERROR: ;
5005#line 53 "wsllib_check.c"
5006  return;
5007}
5008}
Show full sources
↑