Showing error 1985

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

Source: 

1190    if (tmp___0 == 2) {
1191      {
1192#line 19
1193      tmp___1 = isPumpRunning();
1194      }
1195#line 19
1196      if (tmp___1) {
1197
1198      } else {
1199        {
1200#line 16
1201        __automaton_fail();
1202        }
1203      }
1204    } else {
1205
1206    }
1207  }
1208#line 16
1209  return;
1210}
1211}
1212#line 1 "wsllib_check.o"
1213#pragma merger(0,"wsllib_check.i","")
1214#line 3 "wsllib_check.c"
1215void __automaton_fail(void) 
1216{ 
1217
1218  {
1219  goto ERROR;
1220  ERROR: ;
1221#line 53 "wsllib_check.c"
1222  return;
1223}
1224}
1225#line 1 "featureselect.o"
1226#pragma merger(0,"featureselect.i","")
1227#line 8 "featureselect.h"
1228int select_one(void) ;
1229#line 8 "featureselect.c"
1230int select_one(void)
Show full sources
↑