Showing error 222

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: list-properties/simple_built_from_end.cil.c
Line in file: 127
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

 97#line 25
 98    *((struct node **)__cil_tmp10) = p;
 99#line 26
100    p = t;
101  }
102  while_0_break: /* CIL Label */ ;
103  }
104  {
105#line 28
106  while (1) {
107    while_1_continue: /* CIL Label */ ;
108    {
109#line 28
110    __cil_tmp11 = (List )0;
111#line 28
112    __cil_tmp12 = (unsigned int )__cil_tmp11;
113#line 28
114    __cil_tmp13 = (unsigned int )p;
115#line 28
116    if (__cil_tmp13 != __cil_tmp12) {
117
118    } else {
119      goto while_1_break;
120    }
121    }
122    {
123#line 29
124    __cil_tmp14 = *((int *)p);
125#line 29
126    if (__cil_tmp14 != 1) {
127      ERROR: 
128      goto ERROR;
129    } else {
130
131    }
132    }
133#line 32
134    __cil_tmp15 = (unsigned int )p;
135#line 32
136    __cil_tmp16 = __cil_tmp15 + 4;
137#line 32
Show full sources