Showing error 219

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/alternating_list.cil.c
Line in file: 214
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

184        goto ERROR;
185      } else {
186
187      }
188      }
189    } else {
190#line 49
191      flag = 1;
192      {
193#line 50
194      __cil_tmp22 = *((int *)p);
195#line 50
196      if (__cil_tmp22 != 2) {
197        goto ERROR;
198      } else {
199
200      }
201      }
202    }
203#line 53
204    __cil_tmp23 = (unsigned int )p;
205#line 53
206    __cil_tmp24 = __cil_tmp23 + 4;
207#line 53
208    p = *((struct node **)__cil_tmp24);
209  }
210  while_1_break: /* CIL Label */ ;
211  }
212#line 56
213  return (0);
214  ERROR: 
215  {
216#line 59
217  printf("Alternation violation found.\n");
218  }
219#line 60
220  return (1);
221}
222}
Show full sources