Showing error 1640

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

Source: 

 171
 172      } else {
 173        goto while_1_break;
 174      }
 175    } else {
 176      goto while_1_break;
 177    }
 178    {
 179#line 58
 180    timeShift();
 181#line 59
 182    printState();
 183#line 57
 184    i = i + 1;
 185    }
 186  }
 187  while_1_break: /* CIL Label */ ;
 188  }
 189#line 1119 "UnitTests.c"
 190  return;
 191}
 192}
 193#line 1 "wsllib_check.o"
 194#pragma merger(0,"wsllib_check.i","")
 195#line 3 "wsllib_check.c"
 196void __automaton_fail(void) 
 197{ 
 198
 199  {
 200  goto ERROR;
 201  ERROR: ;
 202#line 53 "wsllib_check.c"
 203  return;
 204}
 205}
 206#line 1 "libacc.o"
 207#pragma merger(0,"libacc.i","")
 208#line 73 "/usr/include/assert.h"
 209extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 210                                                                      char const   *__file ,
 211                                                                      unsigned int __line ,
Show full sources
↑