Showing error 1899

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

Source: 

 221#line 17
 222  if (tmp) {
 223    {
 224#line 17
 225    tmp___0 = isPumpRunning();
 226    }
 227#line 17
 228    if (tmp___0) {
 229      {
 230#line 14
 231      __automaton_fail();
 232      }
 233    } else {
 234
 235    }
 236  } else {
 237
 238  }
 239#line 14
 240  return;
 241}
 242}
 243#line 1 "wsllib_check.o"
 244#pragma merger(0,"wsllib_check.i","")
 245#line 3 "wsllib_check.c"
 246void __automaton_fail(void) 
 247{ 
 248
 249  {
 250  goto ERROR;
 251  ERROR: ;
 252#line 53 "wsllib_check.c"
 253  return;
 254}
 255}
 256#line 1 "scenario.o"
 257#pragma merger(0,"scenario.i","")
 258#line 7 "scenario.c"
 259#line 12
 260void stopSystem(void) ;
 261#line 14
Show full sources
↑