Showing error 143

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


Source:

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h"
  5typedef unsigned long size_t;
  6#line 7 "files/rule60_list.c"
  7struct list_head {
  8   struct list_head *prev ;
  9   struct list_head *next ;
 10   int inserted ;
 11};
 12#line 2 "./assert.h"
 13void __blast_assert(void) 
 14{ 
 15
 16  {
 17  ERROR:assert(0); 
 18#line 4
 19  goto ERROR;
 20}
 21}
 22#line 51 "/usr/include/malloc.h"
 23extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 24#line 12 "files/rule60_list.c"
 25static void list_add(struct list_head *new , struct list_head *head ) 
 26{ int __cil_tmp3 ;
 27
 28  {
 29  {
 30#line 13
 31  __cil_tmp3 = new->inserted;
 32#line 13
 33  if (__cil_tmp3 == 0) {
 34
 35  } else {
 36    {
 37#line 13
 38    __blast_assert();
 39    }
 40  }
 41  }
 42#line 14
 43  new->inserted = 1;
 44#line 15
 45  return;
 46}
 47}
 48#line 17 "files/rule60_list.c"
 49static void list_del(struct list_head *entry ) 
 50{ int __cil_tmp2 ;
 51
 52  {
 53  {
 54#line 18
 55  __cil_tmp2 = entry->inserted;
 56#line 18
 57  if (__cil_tmp2 == 1) {
 58
 59  } else {
 60    {
 61#line 18
 62    __blast_assert();
 63    }
 64  }
 65  }
 66#line 19
 67  entry->inserted = 0;
 68#line 20
 69  return;
 70}
 71}
 72#line 22 "files/rule60_list.c"
 73static struct list_head head  ;
 74#line 24 "files/rule60_list.c"
 75int main(void) 
 76{ struct list_head *dev ;
 77  void *tmp ;
 78  size_t __cil_tmp3 ;
 79  void *__cil_tmp4 ;
 80  unsigned int __cil_tmp5 ;
 81  unsigned int __cil_tmp6 ;
 82
 83  {
 84  {
 85#line 26
 86  __cil_tmp3 = (size_t )12U;
 87#line 26
 88  tmp = malloc(__cil_tmp3);
 89#line 26
 90  dev = (struct list_head *)tmp;
 91  }
 92  {
 93#line 27
 94  __cil_tmp4 = (void *)0;
 95#line 27
 96  __cil_tmp5 = (unsigned int )__cil_tmp4;
 97#line 27
 98  __cil_tmp6 = (unsigned int )dev;
 99#line 27
100  if (__cil_tmp6 != __cil_tmp5) {
101    {
102#line 28
103    dev->inserted = 0;
104#line 29
105    list_add(dev, & head);
106#line 30
107    list_del(dev);
108#line 31
109    list_add(dev, & head);
110    }
111  } else {
112
113  }
114  }
115#line 33
116  return (0);
117}
118}