Showing error 1600

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


Source:

 222
 223      } else {
 224        goto while_1_break;
 225      }
 226    } else {
 227      goto while_1_break;
 228    }
 229    {
 230#line 58
 231    timeShift();
 232#line 59
 233    printState();
 234#line 57
 235    i = i + 1;
 236    }
 237  }
 238  while_1_break: /* CIL Label */ ;
 239  }
 240#line 1119 "UnitTests.c"
 241  return;
 242}
 243}
 244#line 1 "wsllib_check.o"
 245#pragma merger(0,"wsllib_check.i","")
 246#line 3 "wsllib_check.c"
 247void __automaton_fail(void) 
 248{ 
 249
 250  {
 251  goto ERROR;
 252  ERROR: ;
 253#line 53 "wsllib_check.c"
 254  return;
 255}
 256}
 257#line 1 "Person.o"
 258#pragma merger(0,"Person.i","")
 259#line 10 "Person.h"
 260int getWeight(int person ) ;
 261#line 14
 262int getDestination(int person ) ;
Show full sources