Showing error 1968

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


Source:

 180#line 85
 181  tmp = valid_product();
 182  }
 183#line 85
 184  if (tmp) {
 185    {
 186#line 86
 187    setup();
 188#line 87
 189    runTest();
 190    }
 191  } else {
 192
 193  }
 194#line 1234 "Test.c"
 195  retValue_acc = 0;
 196#line 1236
 197  return (retValue_acc);
 198#line 1243
 199  return (retValue_acc);
 200}
 201}
 202#line 1 "wsllib_check.o"
 203#pragma merger(0,"wsllib_check.i","")
 204#line 3 "wsllib_check.c"
 205void __automaton_fail(void) 
 206{ 
 207
 208  {
 209  goto ERROR;
 210  ERROR: ;
 211#line 53 "wsllib_check.c"
 212  return;
 213}
 214}
 215#line 1 "Specification2_spec.o"
 216#pragma merger(0,"Specification2_spec.i","")
 217#line 10 "MinePump.h"
 218int isPumpRunning(void) ;
 219#line 10 "Environment.h"
 220int isMethaneLevelCritical(void) ;
Show full sources