Showing error 2067

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


Source:

 115#line 20 "featureselect.c"
 116void select_helpers(void) 
 117{ 
 118
 119  {
 120#line 111 "featureselect.c"
 121  return;
 122}
 123}
 124#line 25 "featureselect.c"
 125int valid_product(void) 
 126{ int retValue_acc ;
 127
 128  {
 129#line 129 "featureselect.c"
 130  retValue_acc = 1;
 131#line 131
 132  return (retValue_acc);
 133#line 138
 134  return (retValue_acc);
 135}
 136}
 137#line 1 "wsllib_check.o"
 138#pragma merger(0,"wsllib_check.i","")
 139#line 3 "wsllib_check.c"
 140void __automaton_fail(void) 
 141{ 
 142
 143  {
 144  goto ERROR;
 145  ERROR: ;
 146#line 53 "wsllib_check.c"
 147  return;
 148}
 149}
 150#line 1 "Test.o"
 151#pragma merger(0,"Test.i","")
 152#line 8 "Test.c"
 153int cleanupTimeShifts  =    4;
 154#line 11 "Test.c"
 155#line 20 "Test.c"
Show full sources