Showing error 2093

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

Source: 

 586#line 17
 587  if (tmp == 0) {
 588    {
 589#line 17
 590    tmp___0 = isPumpRunning();
 591    }
 592#line 17
 593    if (tmp___0) {
 594      {
 595#line 14
 596      __automaton_fail();
 597      }
 598    } else {
 599
 600    }
 601  } else {
 602
 603  }
 604#line 14
 605  return;
 606}
 607}
 608#line 1 "wsllib_check.o"
 609#pragma merger(0,"wsllib_check.i","")
 610#line 3 "wsllib_check.c"
 611void __automaton_fail(void) 
 612{ 
 613
 614  {
 615  goto ERROR;
 616  ERROR: ;
 617#line 53 "wsllib_check.c"
 618  return;
 619}
 620}
 621#line 1 "Environment.o"
 622#pragma merger(0,"Environment.i","")
 623#line 4 "Environment.h"
 624void lowerWaterLevel(void) ;
 625#line 6
 626void waterRise(void) ;
Show full sources
↑