Showing error 2005

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


Source:

 741#line 20 "featureselect.c"
 742void select_helpers(void) 
 743{ 
 744
 745  {
 746#line 111 "featureselect.c"
 747  return;
 748}
 749}
 750#line 25 "featureselect.c"
 751int valid_product(void) 
 752{ int retValue_acc ;
 753
 754  {
 755#line 129 "featureselect.c"
 756  retValue_acc = 1;
 757#line 131
 758  return (retValue_acc);
 759#line 138
 760  return (retValue_acc);
 761}
 762}
 763#line 1 "wsllib_check.o"
 764#pragma merger(0,"wsllib_check.i","")
 765#line 3 "wsllib_check.c"
 766void __automaton_fail(void) 
 767{ 
 768
 769  {
 770  goto ERROR;
 771  ERROR: ;
 772#line 53 "wsllib_check.c"
 773  return;
 774}
 775}
 776#line 1 "libacc.o"
 777#pragma merger(0,"libacc.i","")
 778#line 73 "/usr/include/assert.h"
 779extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 780                                                                      char const   *__file ,
 781                                                                      unsigned int __line ,
Show full sources