Showing error 1447

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


Source:

175  } else {
176    {
177#line 50
178    while (1) {
179      while_2_continue: /* CIL Label */ ;
180      {
181#line 50
182      __cil_tmp22 = *((int *)p);
183#line 50
184      if (__cil_tmp22 == 2) {
185
186      } else {
187        goto while_2_break;
188      }
189      }
190#line 51
191      __cil_tmp23 = (unsigned int )p;
192#line 51
193      __cil_tmp24 = __cil_tmp23 + 4;
194#line 51
195      p = *((struct node **)__cil_tmp24);
196    }
197    while_2_break: /* CIL Label */ ;
198    }
199  }
200  {
201#line 52
202  __cil_tmp25 = *((int *)p);
203#line 52
204  if (__cil_tmp25 != 3) {
205    ERROR: 
206    goto ERROR;
207  } else {
208
209  }
210  }
211#line 54
212  return;
213}
214}
Show full sources