Showing error 2040

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

Source: 

1132#line 17
1133  if (tmp == 0) {
1134    {
1135#line 17
1136    tmp___0 = isPumpRunning();
1137    }
1138#line 17
1139    if (tmp___0) {
1140      {
1141#line 14
1142      __automaton_fail();
1143      }
1144    } else {
1145
1146    }
1147  } else {
1148
1149  }
1150#line 14
1151  return;
1152}
1153}
1154#line 1 "wsllib_check.o"
1155#pragma merger(0,"wsllib_check.i","")
1156#line 3 "wsllib_check.c"
1157void __automaton_fail(void) 
1158{ 
1159
1160  {
1161  goto ERROR;
1162  ERROR: ;
1163#line 53 "wsllib_check.c"
1164  return;
1165}
1166}
1167#line 1 "featureselect.o"
1168#pragma merger(0,"featureselect.i","")
1169#line 8 "featureselect.h"
1170int select_one(void) ;
1171#line 8 "featureselect.c"
1172int select_one(void)
Show full sources
↑