Showing error 1894

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


Source:

 264#line 12
 265      if (tmp___1) {
 266
 267      } else {
 268
 269      }
 270    }
 271    {
 272#line 14
 273    timeShift();
 274    }
 275  }
 276  while_1_break: /* CIL Label */ ;
 277  }
 278  {
 279#line 16
 280  cleanup();
 281  }
 282#line 76 "scenario.c"
 283  return;
 284}
 285}
 286#line 1 "wsllib_check.o"
 287#pragma merger(0,"wsllib_check.i","")
 288#line 3 "wsllib_check.c"
 289void __automaton_fail(void) 
 290{ 
 291
 292  {
 293  goto ERROR;
 294  ERROR: ;
 295#line 53 "wsllib_check.c"
 296  return;
 297}
 298}
 299#line 1 "MinePump.o"
 300#pragma merger(0,"MinePump.i","")
 301#line 4 "Environment.h"
 302void lowerWaterLevel(void) ;
 303#line 10
 304int isMethaneLevelCritical(void) ;
Show full sources