Showing error 1883

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


Source:

 524#line 12
 525        stopSystem();
 526        }
 527      } else {
 528
 529      }
 530    }
 531    {
 532#line 14
 533    timeShift();
 534    }
 535  }
 536  while_0_break: /* CIL Label */ ;
 537  }
 538  {
 539#line 16
 540  cleanup();
 541  }
 542#line 76 "scenario.c"
 543  return;
 544}
 545}
 546#line 1 "wsllib_check.o"
 547#pragma merger(0,"wsllib_check.i","")
 548#line 3 "wsllib_check.c"
 549void __automaton_fail(void) 
 550{ 
 551
 552  {
 553  goto ERROR;
 554  ERROR: ;
 555#line 53 "wsllib_check.c"
 556  return;
 557}
 558}
 559#line 1 "Specification1_spec.o"
 560#pragma merger(0,"Specification1_spec.i","")
 561#line 11 "Specification1_spec.c"
 562void __utac_acc__Specification1_spec__1(void) 
 563{ int tmp ;
 564  int tmp___0 ;
Show full sources