Showing error 1727

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


Source:

4267    }
4268  }
4269#line 903 "libacc.c"
4270  __cil_tmp7 = i - 1;
4271#line 903
4272  __cil_tmp8 = (unsigned long )this;
4273#line 903
4274  __cil_tmp9 = __cil_tmp8 + 24;
4275#line 903
4276  mem_13 = (char const   ***)__cil_tmp9;
4277#line 903
4278  __cil_tmp10 = *mem_13;
4279#line 903
4280  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4281#line 903
4282  retValue_acc = *__cil_tmp11;
4283#line 905
4284  return (retValue_acc);
4285#line 912
4286  return (retValue_acc);
4287}
4288}
4289#line 1 "wsllib_check.o"
4290#pragma merger(0,"wsllib_check.i","")
4291#line 3 "wsllib_check.c"
4292void __automaton_fail(void) 
4293{ 
4294
4295  {
4296  goto ERROR;
4297  ERROR: ;
4298#line 53 "wsllib_check.c"
4299  return;
4300}
4301}
4302#line 1 "featureselect.o"
4303#pragma merger(0,"featureselect.i","")
4304#line 41 "featureselect.h"
4305int select_one(void) ;
4306#line 8 "featureselect.c"
4307int select_one(void) 
Show full sources