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: 

 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}
Show full sources
↑