Showing error 1389

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


Source:

54#line 21
55  *((struct Innermost **)__cil_tmp6) = & im;
56#line 22
57  good_a15 = 1;
58#line 22
59  good_x14 = & inner;
60#line 23
61  __cil_tmp7 = (unsigned int )good_x14;
62#line 23
63  __cil_tmp8 = __cil_tmp7 + 4;
64#line 23
65  __cil_tmp9 = *((struct Innermost **)__cil_tmp8);
66#line 23
67  *((int *)__cil_tmp9) = 4;
68  {
69#line 24
70  __cil_tmp10 = (unsigned int )good_x14;
71#line 24
72  __cil_tmp11 = __cil_tmp10 + 4;
73#line 24
74  __cil_tmp12 = *((struct Innermost **)__cil_tmp11);
75#line 24
76  __cil_tmp13 = *((int *)__cil_tmp12);
77#line 24
78  if (__cil_tmp13 == 4) {
79
80  } else {
81    {
82#line 24
83    //__assert_fail("good.x->y->c == 4", "nested_structure-safe.c", 24U, "main");
84    ERROR: goto ERROR;
85    }
86  }
87  }
88#line 25
89  return (0);
90}
91}
Show full sources