Showing error 1951

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

Source: 

1186#line 355
1187    tmp___0 = 1;
1188  }
1189#line 355
1190  retValue_acc = tmp___0;
1191#line 357
1192  return (retValue_acc);
1193#line 364
1194  return (retValue_acc);
1195}
1196}
1197#line 84 "MinePump.c"
1198void startSystem(void) 
1199{ 
1200
1201  {
1202#line 86
1203  systemActive = 1;
1204#line 388 "MinePump.c"
1205  return;
1206}
1207}
1208#line 1 "wsllib_check.o"
1209#pragma merger(0,"wsllib_check.i","")
1210#line 3 "wsllib_check.c"
1211void __automaton_fail(void) 
1212{ 
1213
1214  {
1215  goto ERROR;
1216  ERROR: ;
1217#line 53 "wsllib_check.c"
1218  return;
1219}
1220}
1221#line 1 "Specification2_spec.o"
1222#pragma merger(0,"Specification2_spec.i","")
1223#line 7 "Specification2_spec.c"
1224int methAndRunningLastTime  ;
1225#line 11 "Specification2_spec.c"
1226void __utac_acc__Specification2_spec__1(void)
Show full sources
↑