Showing error 2142

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


Source:

 249#line 85
 250  tmp = valid_product();
 251  }
 252#line 85
 253  if (tmp) {
 254    {
 255#line 86
 256    setup();
 257#line 87
 258    runTest();
 259    }
 260  } else {
 261
 262  }
 263#line 1234 "Test.c"
 264  retValue_acc = 0;
 265#line 1236
 266  return (retValue_acc);
 267#line 1243
 268  return (retValue_acc);
 269}
 270}
 271#line 1 "wsllib_check.o"
 272#pragma merger(0,"wsllib_check.i","")
 273#line 3 "wsllib_check.c"
 274void __automaton_fail(void) 
 275{ 
 276
 277  {
 278  goto ERROR;
 279  ERROR: ;
 280#line 53 "wsllib_check.c"
 281  return;
 282}
 283}
 284#line 1 "featureselect.o"
 285#pragma merger(0,"featureselect.i","")
 286#line 8 "featureselect.h"
 287int select_one(void) ;
 288#line 8 "featureselect.c"
 289int select_one(void) 
Show full sources