Showing error 1449

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

Source: 

234  while_2_break: /* CIL Label */ ;
235  }
236  {
237#line 44
238  while (1) {
239    while_3_continue: /* CIL Label */ ;
240    {
241#line 44
242    __cil_tmp32 = *((int *)p);
243#line 44
244    if (__cil_tmp32 == 2) {
245
246    } else {
247      goto while_3_break;
248    }
249    }
250#line 45
251    __cil_tmp33 = (unsigned int )p;
252#line 45
253    __cil_tmp34 = __cil_tmp33 + 4;
254#line 45
255    p = *((struct node **)__cil_tmp34);
256  }
257  while_3_break: /* CIL Label */ ;
258  }
259  {
260#line 46
261  __cil_tmp35 = *((int *)p);
262#line 46
263  if (__cil_tmp35 != 3) {
264    ERROR: 
265    goto ERROR;
266  } else {
267
268  }
269  }
270#line 49
271  return;
272}
273}
Show full sources
↑