Showing error 1971

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

Source: 

 379    if (tmp___0 == 2) {
 380      {
 381#line 19
 382      tmp___1 = isPumpRunning();
 383      }
 384#line 19
 385      if (tmp___1) {
 386
 387      } else {
 388        {
 389#line 16
 390        __automaton_fail();
 391        }
 392      }
 393    } else {
 394
 395    }
 396  }
 397#line 16
 398  return;
 399}
 400}
 401#line 1 "wsllib_check.o"
 402#pragma merger(0,"wsllib_check.i","")
 403#line 3 "wsllib_check.c"
 404void __automaton_fail(void) 
 405{ 
 406
 407  {
 408  goto ERROR;
 409  ERROR: ;
 410#line 53 "wsllib_check.c"
 411  return;
 412}
 413}
 414#line 1 "Test.o"
 415#pragma merger(0,"Test.i","")
 416#line 8 "Test.c"
 417int cleanupTimeShifts  =    4;
 418#line 11 "Test.c"
 419#line 17 "Test.c"
Show full sources
↑