Showing error 2004

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

Source: 

1076    if (tmp___0 == 2) {
1077      {
1078#line 19
1079      tmp___1 = isPumpRunning();
1080      }
1081#line 19
1082      if (tmp___1) {
1083
1084      } else {
1085        {
1086#line 16
1087        __automaton_fail();
1088        }
1089      }
1090    } else {
1091
1092    }
1093  }
1094#line 16
1095  return;
1096}
1097}
1098#line 1 "wsllib_check.o"
1099#pragma merger(0,"wsllib_check.i","")
1100#line 3 "wsllib_check.c"
1101void __automaton_fail(void) 
1102{ 
1103
1104  {
1105  goto ERROR;
1106  ERROR: ;
1107#line 53 "wsllib_check.c"
1108  return;
1109}
1110}
1111#line 1 "Environment.o"
1112#pragma merger(0,"Environment.i","")
1113#line 9 "Environment.c"
1114int waterLevel  =    1;
1115#line 12 "Environment.c"
1116int methaneLevelCritical  =    0;
Show full sources
↑