Showing error 1861

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

Source: 

1256
1257  {
1258  {
1259#line 329 "MinePump.c"
1260  tmp = isLowWaterSensorDry();
1261  }
1262#line 329
1263  if (tmp) {
1264#line 329
1265    tmp___0 = 0;
1266  } else {
1267#line 329
1268    tmp___0 = 1;
1269  }
1270#line 329
1271  retValue_acc = tmp___0;
1272#line 331
1273  return (retValue_acc);
1274#line 338
1275  return (retValue_acc);
1276}
1277}
1278#line 1 "wsllib_check.o"
1279#pragma merger(0,"wsllib_check.i","")
1280#line 3 "wsllib_check.c"
1281void __automaton_fail(void) 
1282{ 
1283
1284  {
1285  goto ERROR;
1286  ERROR: ;
1287#line 53 "wsllib_check.c"
1288  return;
1289}
1290}
Show full sources
↑