Showing error 1659

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


Source:

 600#line 20 "featureselect.c"
 601void select_helpers(void) 
 602{ 
 603
 604  {
 605#line 112 "featureselect.c"
 606  return;
 607}
 608}
 609#line 25 "featureselect.c"
 610int valid_product(void) 
 611{ int retValue_acc ;
 612
 613  {
 614#line 130 "featureselect.c"
 615  retValue_acc = 1;
 616#line 132
 617  return (retValue_acc);
 618#line 139
 619  return (retValue_acc);
 620}
 621}
 622#line 1 "wsllib_check.o"
 623#pragma merger(0,"wsllib_check.i","")
 624#line 3 "wsllib_check.c"
 625void __automaton_fail(void) 
 626{ 
 627
 628  {
 629  goto ERROR;
 630  ERROR: ;
 631#line 53 "wsllib_check.c"
 632  return;
 633}
 634}
 635#line 1 "Specification9_spec.o"
 636#pragma merger(0,"Specification9_spec.i","")
 637#line 26 "Elevator.h"
 638int isEmpty(void) ;
 639#line 38
 640int areDoorsOpen(void) ;
Show full sources