Showing error 1880

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


Source:

 647#line 20 "featureselect.c"
 648void select_helpers(void) 
 649{ 
 650
 651  {
 652#line 111 "featureselect.c"
 653  return;
 654}
 655}
 656#line 25 "featureselect.c"
 657int valid_product(void) 
 658{ int retValue_acc ;
 659
 660  {
 661#line 129 "featureselect.c"
 662  retValue_acc = 1;
 663#line 131
 664  return (retValue_acc);
 665#line 138
 666  return (retValue_acc);
 667}
 668}
 669#line 1 "wsllib_check.o"
 670#pragma merger(0,"wsllib_check.i","")
 671#line 3 "wsllib_check.c"
 672void __automaton_fail(void) 
 673{ 
 674
 675  {
 676  goto ERROR;
 677  ERROR: ;
 678#line 53 "wsllib_check.c"
 679  return;
 680}
 681}
 682#line 1 "libacc.o"
 683#pragma merger(0,"libacc.i","")
 684#line 73 "/usr/include/assert.h"
 685extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 686                                                                      char const   *__file ,
 687                                                                      unsigned int __line ,
Show full sources