Showing error 1453

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


Source:

147  __cil_tmp19 = (unsigned int )p;
148#line 31
149  __cil_tmp20 = __cil_tmp19 + 4;
150#line 31
151  *((struct node **)__cil_tmp20) = (struct node *)0;
152#line 32
153  p = a;
154  {
155#line 33
156  while (1) {
157    while_1_continue: /* CIL Label */ ;
158    {
159#line 33
160    __cil_tmp21 = (List )0;
161#line 33
162    __cil_tmp22 = (unsigned int )__cil_tmp21;
163#line 33
164    __cil_tmp23 = (unsigned int )p;
165#line 33
166    if (__cil_tmp23 != __cil_tmp22) {
167
168    } else {
169      goto while_1_break;
170    }
171    }
172    {
173#line 34
174    __cil_tmp24 = *((int *)p);
175#line 34
176    if (__cil_tmp24 != 1) {
177      ERROR: 
178      goto ERROR;
179    } else {
180
181    }
182    }
183#line 37
184    __cil_tmp25 = (unsigned int )p;
185#line 37
186    __cil_tmp26 = __cil_tmp25 + 4;
187#line 37
Show full sources