Showing error 2007

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


Source:

1181}
1182#line 58 "Environment.c"
1183int isHighWaterSensorDry(void) 
1184{ int retValue_acc ;
1185
1186  {
1187#line 65 "Environment.c"
1188  if (waterLevel < 2) {
1189#line 243
1190    retValue_acc = 1;
1191#line 245
1192    return (retValue_acc);
1193  } else {
1194#line 251 "Environment.c"
1195    retValue_acc = 0;
1196#line 253
1197    return (retValue_acc);
1198  }
1199#line 260 "Environment.c"
1200  return (retValue_acc);
1201}
1202}
1203#line 1 "wsllib_check.o"
1204#pragma merger(0,"wsllib_check.i","")
1205#line 3 "wsllib_check.c"
1206void __automaton_fail(void) 
1207{ 
1208
1209  {
1210  goto ERROR;
1211  ERROR: ;
1212#line 53 "wsllib_check.c"
1213  return;
1214}
1215}
1216#line 1 "Specification3_spec.o"
1217#pragma merger(0,"Specification3_spec.i","")
1218#line 11 "Specification3_spec.c"
1219void __utac_acc__Specification3_spec__1(void) 
1220{ int tmp ;
1221  int tmp___0 ;
Show full sources