Showing error 2068

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

Source: 

1195
1196  {
1197  {
1198#line 303 "MinePump.c"
1199  tmp = isHighWaterSensorDry();
1200  }
1201#line 303
1202  if (tmp) {
1203#line 303
1204    tmp___0 = 0;
1205  } else {
1206#line 303
1207    tmp___0 = 1;
1208  }
1209#line 303
1210  retValue_acc = tmp___0;
1211#line 305
1212  return (retValue_acc);
1213#line 312
1214  return (retValue_acc);
1215}
1216}
1217#line 1 "wsllib_check.o"
1218#pragma merger(0,"wsllib_check.i","")
1219#line 3 "wsllib_check.c"
1220void __automaton_fail(void) 
1221{ 
1222
1223  {
1224  goto ERROR;
1225  ERROR: ;
1226#line 53 "wsllib_check.c"
1227  return;
1228}
1229}
1230#line 1 "Specification4_spec.o"
1231#pragma merger(0,"Specification4_spec.i","")
1232#line 11 "Specification4_spec.c"
1233void __utac_acc__Specification4_spec__1(void) 
1234{ int tmp ;
1235  int tmp___0 ;
Show full sources
↑