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 |
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}