Showing error 1941

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

Source: 

1240#line 13
1241        stopSystem();
1242        }
1243      } else {
1244
1245      }
1246    }
1247    {
1248#line 15
1249    timeShift();
1250    }
1251  }
1252  while_4_break: /* CIL Label */ ;
1253  }
1254  {
1255#line 17
1256  cleanup();
1257  }
1258#line 78 "scenario.c"
1259  return;
1260}
1261}
1262#line 1 "wsllib_check.o"
1263#pragma merger(0,"wsllib_check.i","")
1264#line 3 "wsllib_check.c"
1265void __automaton_fail(void) 
1266{ 
1267
1268  {
1269  goto ERROR;
1270  ERROR: ;
1271#line 53 "wsllib_check.c"
1272  return;
1273}
1274}
1275#line 1 "Specification2_spec.o"
1276#pragma merger(0,"Specification2_spec.i","")
1277#line 7 "Specification2_spec.c"
1278int methAndRunningLastTime  ;
1279#line 11 "Specification2_spec.c"
1280void __utac_acc__Specification2_spec__1(void)
Show full sources
↑