Showing error 1929

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

Source: 

1198#line 24
1199      if (methAndRunningLastTime) {
1200        {
1201#line 21
1202        __automaton_fail();
1203        }
1204      } else {
1205#line 23
1206        methAndRunningLastTime = 1;
1207      }
1208    } else {
1209#line 26
1210      methAndRunningLastTime = 0;
1211    }
1212  } else {
1213#line 26
1214    methAndRunningLastTime = 0;
1215  }
1216#line 26
1217  return;
1218}
1219}
1220#line 1 "wsllib_check.o"
1221#pragma merger(0,"wsllib_check.i","")
1222#line 3 "wsllib_check.c"
1223void __automaton_fail(void) 
1224{ 
1225
1226  {
1227  goto ERROR;
1228  ERROR: ;
1229#line 53 "wsllib_check.c"
1230  return;
1231}
1232}
1233#line 1 "Environment.o"
1234#pragma merger(0,"Environment.i","")
1235#line 12 "Environment.h"
1236int getWaterLevel(void) ;
1237#line 9 "Environment.c"
1238int waterLevel  =    1;
Show full sources
↑