Showing error 1395

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/recursive_list.c_unsafe.cil.c
Line in file: 16
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 15 "files/recursive_list.c"
  5struct list {
  6   int n ;
  7   struct list *next ;
  8};
  9#line 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
 10typedef unsigned int size_t;
 11#line 12 "files/recursive_list.c"
 12void err(void) 
 13{ 
 14
 15  {
 16  ERROR: 
 17#line 13
 18  goto ERROR;
 19}
 20}
 21#line 22 "files/recursive_list.c"
 22int i  =    1;
 23#line 471 "/usr/include/stdlib.h"
 24extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 25#line 23 "files/recursive_list.c"
 26void *allocate_memory(void) 
 27{ void *tmp ;
 28  unsigned int __cil_tmp2 ;
 29
 30  {
 31  {
 32#line 25
 33  __cil_tmp2 = (unsigned int )8UL;
 34#line 25
 35  tmp = malloc(__cil_tmp2);
 36  }
 37#line 25
 38  return (tmp);
 39}
 40}
 41#line 28 "files/recursive_list.c"
 42struct list *append(struct list *l , int n ) 
 43{ struct list *new_el ;
 44  void *tmp ;
 45
 46  {
 47  {
 48#line 32
 49  tmp = allocate_memory();
 50#line 32
 51  new_el = (struct list *)tmp;
 52#line 34
 53  new_el->n = n;
 54#line 35
 55  new_el->next = l;
 56  }
 57#line 37
 58  return (new_el);
 59}
 60}
 61#line 40 "files/recursive_list.c"
 62int main(void) 
 63{ struct list *l ;
 64  struct list m ;
 65  struct list *__cil_tmp3 ;
 66  struct list *__cil_tmp4 ;
 67  int __cil_tmp5 ;
 68
 69  {
 70  {
 71#line 43
 72  l = & m;
 73#line 44
 74  l->next = (struct list *)0;
 75#line 45
 76  l->n = 0;
 77#line 47
 78  l = append(l, 1);
 79#line 48
 80  l = append(l, 2);
 81  }
 82  {
 83#line 53
 84  __cil_tmp3 = l->next;
 85#line 53
 86  __cil_tmp4 = __cil_tmp3->next;
 87#line 53
 88  __cil_tmp5 = __cil_tmp4->n;
 89#line 53
 90  if (__cil_tmp5 == 0) {
 91    {
 92#line 53
 93    err();
 94    }
 95  } else {
 96
 97  }
 98  }
 99#line 56
100  return (0);
101}
102}