Showing error 2132

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


Source:

 229#line 85
 230  tmp = valid_product();
 231  }
 232#line 85
 233  if (tmp) {
 234    {
 235#line 86
 236    setup();
 237#line 87
 238    runTest();
 239    }
 240  } else {
 241
 242  }
 243#line 1234 "Test.c"
 244  retValue_acc = 0;
 245#line 1236
 246  return (retValue_acc);
 247#line 1243
 248  return (retValue_acc);
 249}
 250}
 251#line 1 "wsllib_check.o"
 252#pragma merger(0,"wsllib_check.i","")
 253#line 3 "wsllib_check.c"
 254void __automaton_fail(void) 
 255{ 
 256
 257  {
 258  goto ERROR;
 259  ERROR: ;
 260#line 53 "wsllib_check.c"
 261  return;
 262}
 263}
 264#line 1 "MinePump.o"
 265#pragma merger(0,"MinePump.i","")
 266#line 4 "Environment.h"
 267void lowerWaterLevel(void) ;
 268#line 10
 269int isMethaneLevelCritical(void) ;
Show full sources