Showing error 1660

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


Source:

 381
 382      } else {
 383        goto while_1_break;
 384      }
 385    } else {
 386      goto while_1_break;
 387    }
 388    {
 389#line 58
 390    timeShift();
 391#line 59
 392    printState();
 393#line 57
 394    i = i + 1;
 395    }
 396  }
 397  while_1_break: /* CIL Label */ ;
 398  }
 399#line 1123 "UnitTests.c"
 400  return;
 401}
 402}
 403#line 1 "wsllib_check.o"
 404#pragma merger(0,"wsllib_check.i","")
 405#line 3 "wsllib_check.c"
 406void __automaton_fail(void) 
 407{ 
 408
 409  {
 410  goto ERROR;
 411  ERROR: ;
 412#line 53 "wsllib_check.c"
 413  return;
 414}
 415}
 416#line 1 "Floor.o"
 417#pragma merger(0,"Floor.i","")
 418#line 12 "Floor.h"
 419int isFloorCalling(int floorID ) ;
 420#line 14
 421void resetCallOnFloor(int floorID ) ;
Show full sources