Showing error 1641

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


Source:

 309    if (expectedDirection == 1) {
 310      {
 311#line 40
 312      tmp = getCurrentHeading();
 313      }
 314#line 40
 315      if (tmp == 0) {
 316        {
 317#line 41
 318        __automaton_fail();
 319        }
 320      } else {
 321
 322      }
 323    } else {
 324
 325    }
 326  }
 327#line 41
 328  return;
 329}
 330}
 331#line 1 "wsllib_check.o"
 332#pragma merger(0,"wsllib_check.i","")
 333#line 3 "wsllib_check.c"
 334void __automaton_fail(void) 
 335{ 
 336
 337  {
 338  goto ERROR;
 339  ERROR: ;
 340#line 53 "wsllib_check.c"
 341  return;
 342}
 343}
 344#line 1 "Elevator.o"
 345#pragma merger(0,"Elevator.i","")
 346#line 359 "/usr/include/stdio.h"
 347extern int printf(char const   * __restrict  __format  , ...) ;
 348#line 10 "Person.h"
 349int getWeight(int person ) ;
Show full sources