Showing error 2090

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


Source:

 557#line 20 "featureselect.c"
 558void select_helpers(void) 
 559{ 
 560
 561  {
 562#line 111 "featureselect.c"
 563  return;
 564}
 565}
 566#line 25 "featureselect.c"
 567int valid_product(void) 
 568{ int retValue_acc ;
 569
 570  {
 571#line 129 "featureselect.c"
 572  retValue_acc = 1;
 573#line 131
 574  return (retValue_acc);
 575#line 138
 576  return (retValue_acc);
 577}
 578}
 579#line 1 "wsllib_check.o"
 580#pragma merger(0,"wsllib_check.i","")
 581#line 3 "wsllib_check.c"
 582void __automaton_fail(void) 
 583{ 
 584
 585  {
 586  goto ERROR;
 587  ERROR: ;
 588#line 53 "wsllib_check.c"
 589  return;
 590}
 591}
 592#line 1 "Test.o"
 593#pragma merger(0,"Test.i","")
 594#line 8 "Test.c"
 595int cleanupTimeShifts  =    4;
 596#line 11 "Test.c"
 597#line 17 "Test.c"
Show full sources