Showing error 2115

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


Source:

1202  }
1203  {
1204#line 51
1205  printf(")");
1206  }
1207#line 189 "Environment.c"
1208  return;
1209}
1210}
1211#line 55 "Environment.c"
1212int getWaterLevel(void) 
1213{ int retValue_acc ;
1214
1215  {
1216#line 207 "Environment.c"
1217  retValue_acc = waterLevel;
1218#line 209
1219  return (retValue_acc);
1220#line 216
1221  return (retValue_acc);
1222}
1223}
1224#line 1 "wsllib_check.o"
1225#pragma merger(0,"wsllib_check.i","")
1226#line 3 "wsllib_check.c"
1227void __automaton_fail(void) 
1228{ 
1229
1230  {
1231  goto ERROR;
1232  ERROR: ;
1233#line 53 "wsllib_check.c"
1234  return;
1235}
1236}
1237#line 1 "Specification5_spec.o"
1238#pragma merger(0,"Specification5_spec.i","")
1239#line 7 "Specification5_spec.c"
1240int switchedOnBeforeTS  ;
1241#line 11 "Specification5_spec.c"
1242void __utac_acc__Specification5_spec__1(void) 
Show full sources