Showing error 1445

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

Source: 

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