Showing error 2121

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

Source: 

 251    }
 252#line 31
 253    if (tmp___0) {
 254#line 31
 255      if (! switchedOnBeforeTS) {
 256        {
 257#line 28
 258        __automaton_fail();
 259        }
 260      } else {
 261
 262      }
 263    } else {
 264
 265    }
 266  } else {
 267
 268  }
 269#line 28
 270  return;
 271}
 272}
 273#line 1 "wsllib_check.o"
 274#pragma merger(0,"wsllib_check.i","")
 275#line 3 "wsllib_check.c"
 276void __automaton_fail(void) 
 277{ 
 278
 279  {
 280  goto ERROR;
 281  ERROR: ;
 282#line 53 "wsllib_check.c"
 283  return;
 284}
 285}
 286#line 1 "Environment.o"
 287#pragma merger(0,"Environment.i","")
 288#line 4 "Environment.h"
 289void lowerWaterLevel(void) ;
 290#line 10
 291int isMethaneLevelCritical(void) ;
Show full sources
↑