Showing error 1886

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


Source:

 608#line 20 "featureselect.c"
 609void select_helpers(void) 
 610{ 
 611
 612  {
 613#line 111 "featureselect.c"
 614  return;
 615}
 616}
 617#line 25 "featureselect.c"
 618int valid_product(void) 
 619{ int retValue_acc ;
 620
 621  {
 622#line 129 "featureselect.c"
 623  retValue_acc = 1;
 624#line 131
 625  return (retValue_acc);
 626#line 138
 627  return (retValue_acc);
 628}
 629}
 630#line 1 "wsllib_check.o"
 631#pragma merger(0,"wsllib_check.i","")
 632#line 3 "wsllib_check.c"
 633void __automaton_fail(void) 
 634{ 
 635
 636  {
 637  goto ERROR;
 638  ERROR: ;
 639#line 53 "wsllib_check.c"
 640  return;
 641}
 642}
 643#line 1 "Specification1_spec.o"
 644#pragma merger(0,"Specification1_spec.i","")
 645#line 11 "Specification1_spec.c"
 646void __utac_acc__Specification1_spec__1(void) 
 647{ int tmp ;
 648  int tmp___0 ;
Show full sources