Showing error 1387

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/nested_structure_ptr_safe.cil.c
Line in file: 109
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 9 "nested_structure_ptr-safe.c"
  5struct Innermost {
  6   int c ;
  7};
  8#line 9 "nested_structure_ptr-safe.c"
  9struct Inner {
 10   int b ;
 11   struct Innermost *y ;
 12};
 13#line 9 "nested_structure_ptr-safe.c"
 14struct Toplev {
 15   int a ;
 16   struct Inner *x ;
 17};
 18#line 71 "/usr/include/assert.h"
 19extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 20                                                                      char const   *__file ,
 21                                                                      unsigned int __line ,
 22                                                                      char const   *__function ) ;
 23#line 7 "nested_structure_ptr-safe.c"
 24
 25#line 19 "nested_structure_ptr-safe.c"
 26int main(void) 
 27{ struct Innermost im ;
 28  struct Inner inner ;
 29  struct Toplev good ;
 30  struct Toplev *ptr ;
 31  struct Innermost *__cil_tmp5 ;
 32  struct Inner *__cil_tmp6 ;
 33  unsigned int __cil_tmp7 ;
 34  struct Toplev *__cil_tmp8 ;
 35  unsigned int __cil_tmp9 ;
 36  unsigned int __cil_tmp10 ;
 37  unsigned int __cil_tmp11 ;
 38  struct Inner *__cil_tmp12 ;
 39  unsigned int __cil_tmp13 ;
 40  unsigned int __cil_tmp14 ;
 41  struct Innermost *__cil_tmp15 ;
 42  unsigned int __cil_tmp16 ;
 43  unsigned int __cil_tmp17 ;
 44  struct Inner *__cil_tmp18 ;
 45  unsigned int __cil_tmp19 ;
 46  unsigned int __cil_tmp20 ;
 47  struct Innermost *__cil_tmp21 ;
 48  int __cil_tmp22 ;
 49
 50  {
 51#line 21
 52  __cil_tmp5 = & im;
 53#line 21
 54  *((int *)__cil_tmp5) = 3;
 55#line 22
 56  __cil_tmp6 = & inner;
 57#line 22
 58  *((int *)__cil_tmp6) = 2;
 59#line 22
 60  __cil_tmp7 = (unsigned int )(& inner) + 4;
 61#line 22
 62  *((struct Innermost **)__cil_tmp7) = & im;
 63#line 23
 64  __cil_tmp8 = & good;
 65#line 23
 66  *((int *)__cil_tmp8) = 1;
 67#line 23
 68  __cil_tmp9 = (unsigned int )(& good) + 4;
 69#line 23
 70  *((struct Inner **)__cil_tmp9) = & inner;
 71#line 24
 72  ptr = & good;
 73#line 25
 74  __cil_tmp10 = (unsigned int )ptr;
 75#line 25
 76  __cil_tmp11 = __cil_tmp10 + 4;
 77#line 25
 78  __cil_tmp12 = *((struct Inner **)__cil_tmp11);
 79#line 25
 80  __cil_tmp13 = (unsigned int )__cil_tmp12;
 81#line 25
 82  __cil_tmp14 = __cil_tmp13 + 4;
 83#line 25
 84  __cil_tmp15 = *((struct Innermost **)__cil_tmp14);
 85#line 25
 86  *((int *)__cil_tmp15) = 4;
 87  {
 88#line 26
 89  __cil_tmp16 = (unsigned int )ptr;
 90#line 26
 91  __cil_tmp17 = __cil_tmp16 + 4;
 92#line 26
 93  __cil_tmp18 = *((struct Inner **)__cil_tmp17);
 94#line 26
 95  __cil_tmp19 = (unsigned int )__cil_tmp18;
 96#line 26
 97  __cil_tmp20 = __cil_tmp19 + 4;
 98#line 26
 99  __cil_tmp21 = *((struct Innermost **)__cil_tmp20);
100#line 26
101  __cil_tmp22 = *((int *)__cil_tmp21);
102#line 26
103  if (__cil_tmp22 == 4) {
104
105  } else {
106    {
107#line 26
108    //__assert_fail("ptr->x->y->c == 4", "nested_structure_ptr-safe.c", 26U, "main");
109    ERROR: goto ERROR;
110    }
111  }
112  }
113#line 27
114  return (0);
115}
116}
↑