Showing error 2159

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


Source:

1133    }
1134  }
1135#line 903 "libacc.c"
1136  __cil_tmp7 = i - 1;
1137#line 903
1138  __cil_tmp8 = (unsigned long )this;
1139#line 903
1140  __cil_tmp9 = __cil_tmp8 + 24;
1141#line 903
1142  mem_13 = (char const   ***)__cil_tmp9;
1143#line 903
1144  __cil_tmp10 = *mem_13;
1145#line 903
1146  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1147#line 903
1148  retValue_acc = *__cil_tmp11;
1149#line 905
1150  return (retValue_acc);
1151#line 912
1152  return (retValue_acc);
1153}
1154}
1155#line 1 "wsllib_check.o"
1156#pragma merger(0,"wsllib_check.i","")
1157#line 3 "wsllib_check.c"
1158void __automaton_fail(void) 
1159{ 
1160
1161  {
1162  goto ERROR;
1163  ERROR: ;
1164#line 53 "wsllib_check.c"
1165  return;
1166}
1167}
1168#line 1 "Specification5_spec.o"
1169#pragma merger(0,"Specification5_spec.i","")
1170#line 7 "Specification5_spec.c"
1171int switchedOnBeforeTS  ;
1172#line 11 "Specification5_spec.c"
1173__inline void __utac_acc__Specification5_spec__1(void) 
Show full sources