Showing error 1864

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

Source: 

 724#line 17
 725  if (tmp) {
 726    {
 727#line 17
 728    tmp___0 = isPumpRunning();
 729    }
 730#line 17
 731    if (tmp___0) {
 732      {
 733#line 14
 734      __automaton_fail();
 735      }
 736    } else {
 737
 738    }
 739  } else {
 740
 741  }
 742#line 14
 743  return;
 744}
 745}
 746#line 1 "wsllib_check.o"
 747#pragma merger(0,"wsllib_check.i","")
 748#line 3 "wsllib_check.c"
 749void __automaton_fail(void) 
 750{ 
 751
 752  {
 753  goto ERROR;
 754  ERROR: ;
 755#line 53 "wsllib_check.c"
 756  return;
 757}
 758}
 759#line 1 "scenario.o"
 760#pragma merger(0,"scenario.i","")
 761#line 7 "scenario.c"
 762#line 11
 763void startSystem(void) ;
 764#line 13
Show full sources
↑