Showing error 1988

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

Source: 

1249    if (tmp___0 == 2) {
1250      {
1251#line 19
1252      tmp___1 = isPumpRunning();
1253      }
1254#line 19
1255      if (tmp___1) {
1256
1257      } else {
1258        {
1259#line 16
1260        __automaton_fail();
1261        }
1262      }
1263    } else {
1264
1265    }
1266  }
1267#line 16
1268  return;
1269}
1270}
1271#line 1 "wsllib_check.o"
1272#pragma merger(0,"wsllib_check.i","")
1273#line 3 "wsllib_check.c"
1274void __automaton_fail(void) 
1275{ 
1276
1277  {
1278  goto ERROR;
1279  ERROR: ;
1280#line 53 "wsllib_check.c"
1281  return;
1282}
1283}
Show full sources
↑