Showing error 1923

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

Source: 

1265#line 24
1266      if (methAndRunningLastTime) {
1267        {
1268#line 21
1269        __automaton_fail();
1270        }
1271      } else {
1272#line 23
1273        methAndRunningLastTime = 1;
1274      }
1275    } else {
1276#line 26
1277      methAndRunningLastTime = 0;
1278    }
1279  } else {
1280#line 26
1281    methAndRunningLastTime = 0;
1282  }
1283#line 26
1284  return;
1285}
1286}
1287#line 1 "wsllib_check.o"
1288#pragma merger(0,"wsllib_check.i","")
1289#line 3 "wsllib_check.c"
1290void __automaton_fail(void) 
1291{ 
1292
1293  {
1294  goto ERROR;
1295  ERROR: ;
1296#line 53 "wsllib_check.c"
1297  return;
1298}
1299}
Show full sources
↑