Showing error 2010

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

Source: 

 277    if (tmp___0 == 2) {
 278      {
 279#line 19
 280      tmp___1 = isPumpRunning();
 281      }
 282#line 19
 283      if (tmp___1) {
 284
 285      } else {
 286        {
 287#line 16
 288        __automaton_fail();
 289        }
 290      }
 291    } else {
 292
 293    }
 294  }
 295#line 16
 296  return;
 297}
 298}
 299#line 1 "wsllib_check.o"
 300#pragma merger(0,"wsllib_check.i","")
 301#line 3 "wsllib_check.c"
 302void __automaton_fail(void) 
 303{ 
 304
 305  {
 306  goto ERROR;
 307  ERROR: ;
 308#line 53 "wsllib_check.c"
 309  return;
 310}
 311}
 312#line 1 "Environment.o"
 313#pragma merger(0,"Environment.i","")
 314#line 4 "Environment.h"
 315void lowerWaterLevel(void) ;
 316#line 15
 317void printEnvironment(void) ;
Show full sources
↑