Showing error 1890

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

Source: 

 510#line 12
 511      if (tmp___1) {
 512
 513      } else {
 514
 515      }
 516    }
 517    {
 518#line 14
 519    timeShift();
 520    }
 521  }
 522  while_1_break: /* CIL Label */ ;
 523  }
 524  {
 525#line 16
 526  cleanup();
 527  }
 528#line 76 "scenario.c"
 529  return;
 530}
 531}
 532#line 1 "wsllib_check.o"
 533#pragma merger(0,"wsllib_check.i","")
 534#line 3 "wsllib_check.c"
 535void __automaton_fail(void) 
 536{ 
 537
 538  {
 539  goto ERROR;
 540  ERROR: ;
 541#line 53 "wsllib_check.c"
 542  return;
 543}
 544}
 545#line 1 "MinePump.o"
 546#pragma merger(0,"MinePump.i","")
 547#line 6 "MinePump.h"
 548void activatePump(void) ;
 549#line 8
 550void deactivatePump(void) ;
Show full sources
↑