ClabureDB: Classified Bug-Reports Database

  /* Generated by CIL v. 1.3.7 */
  /* print_CIL_Input is true */
  
  #line 211 "/usr/lib/gcc/x86_64-pc-linux-gnu/4.5.3/include/stddef.h"
  typedef unsigned int size_t;
  #line 15 "dll_of_dll_BUG.c"
  struct slave_item {
     struct slave_item *next ;
     struct slave_item *prev ;
 };
 #line 31 "dll_of_dll_BUG.c"
 struct master_item {
    struct master_item *next ;
    struct master_item *prev ;
    struct slave_item *slave ;
 };
 #line 471 "/usr/include/stdlib.h"
 extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 #line 488
 extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
 #line 514
 extern  __attribute__((__nothrow__, __noreturn__)) void abort(void) ;
 #line 3 "dll_of_dll_BUG.c"
 extern int __VERIFIER_nondet_int(void) ;
 #line 5 "dll_of_dll_BUG.c"
 static void fail(void) 
 { 
 
   {
   ERROR: 
   goto ERROR;
 }
 }
 #line 20 "dll_of_dll_BUG.c"
 struct slave_item *alloc_or_die_slave(void) 
 { struct slave_item *ptr ;
   void *tmp ;
   unsigned int __cil_tmp3 ;
   void *__cil_tmp4 ;
   void *__cil_tmp5 ;
 
   {
   {
 #line 22
   __cil_tmp3 = (unsigned int )8UL;
 #line 22
   tmp = malloc(__cil_tmp3);
 #line 22
   ptr = (struct slave_item *)tmp;
   }
 #line 23
   if (! ptr) {
     {
 #line 24
     abort();
     }
   } else {
 
   }
 #line 26
   __cil_tmp4 = (void *)0;
 #line 26
   *((struct slave_item **)ptr) = (struct slave_item *)__cil_tmp4;
 #line 27
   __cil_tmp5 = (void *)0;
 #line 27
   *((struct slave_item **)ptr) = (struct slave_item *)__cil_tmp5;
 #line 28
   return (ptr);
 }
 }
 #line 37 "dll_of_dll_BUG.c"
 struct master_item *alloc_or_die_master(void) 
 { struct master_item *ptr ;
   void *tmp ;
   unsigned int __cil_tmp3 ;
   void *__cil_tmp4 ;
   unsigned int __cil_tmp5 ;
   unsigned int __cil_tmp6 ;
   void *__cil_tmp7 ;
   unsigned int __cil_tmp8 ;
   unsigned int __cil_tmp9 ;
   void *__cil_tmp10 ;
 
   {
   {
 #line 39
   __cil_tmp3 = (unsigned int )12UL;
 #line 39
   tmp = malloc(__cil_tmp3);
 #line 39
   ptr = (struct master_item *)tmp;
   }
 #line 40
   if (! ptr) {
     {
 #line 41
     abort();
     }
  } else {

  }
#line 43
  __cil_tmp4 = (void *)0;
#line 43
  *((struct master_item **)ptr) = (struct master_item *)__cil_tmp4;
#line 44
  __cil_tmp5 = (unsigned int )ptr;
#line 44
  __cil_tmp6 = __cil_tmp5 + 4;
#line 44
  __cil_tmp7 = (void *)0;
#line 44
  *((struct master_item **)__cil_tmp6) = (struct master_item *)__cil_tmp7;
#line 45
  __cil_tmp8 = (unsigned int )ptr;
#line 45
  __cil_tmp9 = __cil_tmp8 + 8;
#line 45
  __cil_tmp10 = (void *)0;
#line 45
  *((struct slave_item **)__cil_tmp9) = (struct slave_item *)__cil_tmp10;
#line 46
  return (ptr);
}
}
#line 49 "dll_of_dll_BUG.c"
void dll_insert_slave(struct slave_item **dll ) 
{ struct slave_item *item ;
  struct slave_item *tmp ;
  struct slave_item *next ;
  unsigned int __cil_tmp5 ;
  unsigned int __cil_tmp6 ;

  {
  {
#line 51
  tmp = alloc_or_die_slave();
#line 51
  item = tmp;
#line 52
  next = *dll;
#line 53
  *((struct slave_item **)item) = next;
  }
#line 54
  if (next) {
#line 55
    __cil_tmp5 = (unsigned int )next;
#line 55
    __cil_tmp6 = __cil_tmp5 + 4;
#line 55
    *((struct slave_item **)__cil_tmp6) = item;
  } else {

  }
#line 57
  *dll = item;
#line 58
  return;
}
}
#line 60 "dll_of_dll_BUG.c"
void *dll_create_generic(void (*insert_fnc)() ) 
{ void *dll ;
  int tmp ;
  void **__cil_tmp4 ;
  void **__cil_tmp5 ;

  {
  {
#line 62
  __cil_tmp4 = & dll;
#line 62
  *__cil_tmp4 = (void *)0;
#line 63
  (*insert_fnc)(& dll);
#line 64
  (*insert_fnc)(& dll);
  }
  {
#line 66
  while (1) {
    while_0_continue: /* CIL Label */ ;
    {
#line 66
    tmp = __VERIFIER_nondet_int();
    }
#line 66
    if (tmp) {

    } else {
      goto while_0_break;
    }
    {
#line 67
    (*insert_fnc)(& dll);
    }
  }
  while_0_break: /* CIL Label */ ;
  }
  {
#line 69
  __cil_tmp5 = & dll;
#line 69
  return (*__cil_tmp5);
  }
}
}
#line 72 "dll_of_dll_BUG.c"
struct slave_item *dll_create_slave(void) 
{ void *tmp ;
  void (*__cil_tmp2)() ;

  {
  {
#line 74
  __cil_tmp2 = (void (*)())(& dll_insert_slave);
#line 74
  tmp = dll_create_generic(__cil_tmp2);
  }
#line 74
  return ((struct slave_item *)tmp);
}
}
#line 77 "dll_of_dll_BUG.c"
void dll_destroy_slave(struct slave_item *dll ) 
{ struct slave_item *next ;
  void *__cil_tmp3 ;

  {
  {
#line 79
  while (1) {
    while_1_continue: /* CIL Label */ ;
#line 79
    if (dll) {

    } else {
      goto while_1_break;
    }
    {
#line 80
    next = *((struct slave_item **)dll);
#line 81
    __cil_tmp3 = (void *)dll;
#line 81
    free(__cil_tmp3);
#line 82
    dll = next;
    }
  }
  while_1_break: /* CIL Label */ ;
  }
#line 84
  return;
}
}
#line 86 "dll_of_dll_BUG.c"
void dll_destroy_nested_lists(struct master_item *dll ) 
{ unsigned int __cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  struct slave_item *__cil_tmp4 ;

  {
  {
#line 88
  while (1) {
    while_2_continue: /* CIL Label */ ;
#line 88
    if (dll) {

    } else {
      goto while_2_break;
    }
    {
#line 89
    __cil_tmp2 = (unsigned int )dll;
#line 89
    __cil_tmp3 = __cil_tmp2 + 8;
#line 89
    __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
#line 89
    dll_destroy_slave(__cil_tmp4);
#line 90
    dll = *((struct master_item **)dll);
    }
  }
  while_2_break: /* CIL Label */ ;
  }
#line 92
  return;
}
}
#line 94 "dll_of_dll_BUG.c"
void dll_reinit_nested_lists(struct master_item *dll ) 
{ unsigned int __cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  void *__cil_tmp4 ;

  {
  {
#line 96
  while (1) {
    while_3_continue: /* CIL Label */ ;
#line 96
    if (dll) {

    } else {
      goto while_3_break;
    }
#line 97
    __cil_tmp2 = (unsigned int )dll;
#line 97
    __cil_tmp3 = __cil_tmp2 + 8;
#line 97
    __cil_tmp4 = (void *)0;
#line 97
    *((struct slave_item **)__cil_tmp3) = (struct slave_item *)__cil_tmp4;
#line 98
    dll = *((struct master_item **)dll);
  }
  while_3_break: /* CIL Label */ ;
  }
#line 100
  return;
}
}
#line 102 "dll_of_dll_BUG.c"
void dll_destroy_master(struct master_item *dll ) 
{ struct master_item *next ;
  void *__cil_tmp3 ;

  {
  {
#line 104
  while (1) {
    while_4_continue: /* CIL Label */ ;
#line 104
    if (dll) {

    } else {
      goto while_4_break;
    }
    {
#line 105
    next = *((struct master_item **)dll);
#line 106
    __cil_tmp3 = (void *)dll;
#line 106
    free(__cil_tmp3);
#line 107
    dll = next;
    }
  }
  while_4_break: /* CIL Label */ ;
  }
#line 109
  return;
}
}
#line 111 "dll_of_dll_BUG.c"
void dll_insert_master(struct master_item **dll ) 
{ struct master_item *item ;
  struct master_item *tmp ;
  struct master_item *next ;
  unsigned int __cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  unsigned int __cil_tmp8 ;

  {
  {
#line 113
  tmp = alloc_or_die_master();
#line 113
  item = tmp;
#line 114
  next = *dll;
#line 115
  *((struct master_item **)item) = next;
  }
#line 116
  if (next) {
#line 117
    __cil_tmp5 = (unsigned int )next;
#line 117
    __cil_tmp6 = __cil_tmp5 + 4;
#line 117
    *((struct master_item **)__cil_tmp6) = item;
  } else {

  }
  {
#line 119
  __cil_tmp7 = (unsigned int )item;
#line 119
  __cil_tmp8 = __cil_tmp7 + 8;
#line 119
  *((struct slave_item **)__cil_tmp8) = dll_create_slave();
#line 120
  *dll = item;
  }
#line 121
  return;
}
}
#line 123 "dll_of_dll_BUG.c"
struct master_item *dll_create_master(void) 
{ void *tmp ;
  void (*__cil_tmp2)() ;

  {
  {
#line 125
  __cil_tmp2 = (void (*)())(& dll_insert_master);
#line 125
  tmp = dll_create_generic(__cil_tmp2);
  }
#line 125
  return ((struct master_item *)tmp);
}
}
#line 128 "dll_of_dll_BUG.c"
void inspect_base(struct master_item *dll ) 
{ struct master_item *__cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  struct master_item *__cil_tmp5 ;
  int __cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  struct master_item *__cil_tmp9 ;
  unsigned int __cil_tmp10 ;
  unsigned int __cil_tmp11 ;
  struct master_item *__cil_tmp12 ;
  struct master_item *__cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  unsigned int __cil_tmp16 ;
  struct master_item *__cil_tmp17 ;
  struct master_item *__cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  int __cil_tmp20 ;

  {
  {
#line 130
  while (1) {
    while_5_continue: /* CIL Label */ ;
#line 130
    if (! dll) {
      {
#line 130
      fail();
      }
    } else {

    }
    goto while_5_break;
  }
  while_5_break: /* CIL Label */ ;
  }
  {
#line 131
  while (1) {
    while_6_continue: /* CIL Label */ ;
    {
#line 131
    __cil_tmp2 = *((struct master_item **)dll);
#line 131
    if (! __cil_tmp2) {
      {
#line 131
      fail();
      }
    } else {

    }
    }
    goto while_6_break;
  }
  while_6_break: /* CIL Label */ ;
  }
  {
#line 132
  while (1) {
    while_7_continue: /* CIL Label */ ;
    {
#line 132
    __cil_tmp3 = (unsigned int )dll;
#line 132
    __cil_tmp4 = __cil_tmp3 + 4;
#line 132
    __cil_tmp5 = *((struct master_item **)__cil_tmp4);
#line 132
    __cil_tmp6 = ! __cil_tmp5;
#line 132
    if (! __cil_tmp6) {
      {
#line 132
      fail();
      }
    } else {

    }
    }
    goto while_7_break;
  }
  while_7_break: /* CIL Label */ ;
  }
#line 134
  dll = *((struct master_item **)dll);
  {
#line 134
  while (1) {
    while_8_continue: /* CIL Label */ ;
#line 134
    if (dll) {

    } else {
      goto while_8_break;
    }
    {
#line 135
    while (1) {
      while_9_continue: /* CIL Label */ ;
      {
#line 135
      __cil_tmp7 = (unsigned int )dll;
#line 135
      __cil_tmp8 = __cil_tmp7 + 4;
#line 135
      __cil_tmp9 = *((struct master_item **)__cil_tmp8);
#line 135
      if (! __cil_tmp9) {
        {
#line 135
        fail();
        }
      } else {

      }
      }
      goto while_9_break;
    }
    while_9_break: /* CIL Label */ ;
    }
    {
#line 136
    while (1) {
      while_10_continue: /* CIL Label */ ;
      {
#line 136
      __cil_tmp10 = (unsigned int )dll;
#line 136
      __cil_tmp11 = __cil_tmp10 + 4;
#line 136
      __cil_tmp12 = *((struct master_item **)__cil_tmp11);
#line 136
      __cil_tmp13 = *((struct master_item **)__cil_tmp12);
#line 136
      if (! __cil_tmp13) {
        {
#line 136
        fail();
        }
      } else {

      }
      }
      goto while_10_break;
    }
    while_10_break: /* CIL Label */ ;
    }
    {
#line 137
    while (1) {
      while_11_continue: /* CIL Label */ ;
      {
#line 137
      __cil_tmp14 = (unsigned int )dll;
#line 137
      __cil_tmp15 = (unsigned int )dll;
#line 137
      __cil_tmp16 = __cil_tmp15 + 4;
#line 137
      __cil_tmp17 = *((struct master_item **)__cil_tmp16);
#line 137
      __cil_tmp18 = *((struct master_item **)__cil_tmp17);
#line 137
      __cil_tmp19 = (unsigned int )__cil_tmp18;
#line 137
      __cil_tmp20 = __cil_tmp19 == __cil_tmp14;
#line 137
      if (! __cil_tmp20) {
        {
#line 137
        fail();
        }
      } else {

      }
      }
      goto while_11_break;
    }
    while_11_break: /* CIL Label */ ;
    }
#line 134
    dll = *((struct master_item **)dll);
  }
  while_8_break: /* CIL Label */ ;
  }
#line 139
  return;
}
}
#line 141 "dll_of_dll_BUG.c"
void inspect_full(struct master_item *dll ) 
{ struct slave_item *pos ;
  unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  struct slave_item *__cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  struct slave_item *__cil_tmp8 ;
  int __cil_tmp9 ;
  unsigned int __cil_tmp10 ;
  unsigned int __cil_tmp11 ;
  struct slave_item *__cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  struct slave_item *__cil_tmp15 ;
  struct slave_item *__cil_tmp16 ;
  unsigned int __cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  struct slave_item *__cil_tmp20 ;
  struct slave_item *__cil_tmp21 ;
  unsigned int __cil_tmp22 ;
  int __cil_tmp23 ;

  {
  {
#line 143
  inspect_base(dll);
  }
  {
#line 145
  while (1) {
    while_12_continue: /* CIL Label */ ;
#line 145
    if (dll) {

    } else {
      goto while_12_break;
    }
#line 146
    __cil_tmp3 = (unsigned int )dll;
#line 146
    __cil_tmp4 = __cil_tmp3 + 8;
#line 146
    pos = *((struct slave_item **)__cil_tmp4);
    {
#line 147
    while (1) {
      while_13_continue: /* CIL Label */ ;
#line 147
      if (! pos) {
        {
#line 147
        fail();
        }
      } else {

      }
      goto while_13_break;
    }
    while_13_break: /* CIL Label */ ;
    }
    {
#line 148
    while (1) {
      while_14_continue: /* CIL Label */ ;
      {
#line 148
      __cil_tmp5 = *((struct slave_item **)pos);
#line 148
      if (! __cil_tmp5) {
        {
#line 148
        fail();
        }
      } else {

      }
      }
      goto while_14_break;
    }
    while_14_break: /* CIL Label */ ;
    }
    {
#line 149
    while (1) {
      while_15_continue: /* CIL Label */ ;
      {
#line 149
      __cil_tmp6 = (unsigned int )pos;
#line 149
      __cil_tmp7 = __cil_tmp6 + 4;
#line 149
      __cil_tmp8 = *((struct slave_item **)__cil_tmp7);
#line 149
      __cil_tmp9 = ! __cil_tmp8;
#line 149
      if (! __cil_tmp9) {
        {
#line 149
        fail();
        }
      } else {

      }
      }
      goto while_15_break;
    }
    while_15_break: /* CIL Label */ ;
    }
#line 151
    pos = *((struct slave_item **)pos);
    {
#line 151
    while (1) {
      while_16_continue: /* CIL Label */ ;
#line 151
      if (pos) {

      } else {
        goto while_16_break;
      }
      {
#line 152
      while (1) {
        while_17_continue: /* CIL Label */ ;
        {
#line 152
        __cil_tmp10 = (unsigned int )pos;
#line 152
        __cil_tmp11 = __cil_tmp10 + 4;
#line 152
        __cil_tmp12 = *((struct slave_item **)__cil_tmp11);
#line 152
        if (! __cil_tmp12) {
          {
#line 152
          fail();
          }
        } else {

        }
        }
        goto while_17_break;
      }
      while_17_break: /* CIL Label */ ;
      }
      {
#line 153
      while (1) {
        while_18_continue: /* CIL Label */ ;
        {
#line 153
        __cil_tmp13 = (unsigned int )pos;
#line 153
        __cil_tmp14 = __cil_tmp13 + 4;
#line 153
        __cil_tmp15 = *((struct slave_item **)__cil_tmp14);
#line 153
        __cil_tmp16 = *((struct slave_item **)__cil_tmp15);
#line 153
        if (! __cil_tmp16) {
          {
#line 153
          fail();
          }
        } else {

        }
        }
        goto while_18_break;
      }
      while_18_break: /* CIL Label */ ;
      }
      {
#line 154
      while (1) {
        while_19_continue: /* CIL Label */ ;
        {
#line 154
        __cil_tmp17 = (unsigned int )pos;
#line 154
        __cil_tmp18 = (unsigned int )pos;
#line 154
        __cil_tmp19 = __cil_tmp18 + 4;
#line 154
        __cil_tmp20 = *((struct slave_item **)__cil_tmp19);
#line 154
        __cil_tmp21 = *((struct slave_item **)__cil_tmp20);
#line 154
        __cil_tmp22 = (unsigned int )__cil_tmp21;
#line 154
        __cil_tmp23 = __cil_tmp22 == __cil_tmp17;
#line 154
        if (! __cil_tmp23) {
          {
#line 154
          fail();
          }
        } else {

        }
        }
        goto while_19_break;
      }
      while_19_break: /* CIL Label */ ;
      }
#line 151
      pos = *((struct slave_item **)pos);
    }
    while_16_break: /* CIL Label */ ;
    }
#line 145
    dll = *((struct master_item **)dll);
  }
  while_12_break: /* CIL Label */ ;
  }
#line 157
  return;
}
}
#line 159 "dll_of_dll_BUG.c"
void inspect_dangling(struct master_item *dll ) 
{ unsigned int __cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  struct slave_item *__cil_tmp4 ;

  {
  {
#line 161
  inspect_base(dll);
  }
  {
#line 163
  while (1) {
    while_20_continue: /* CIL Label */ ;
#line 163
    if (dll) {

    } else {
      goto while_20_break;
    }
    {
#line 164
    while (1) {
      while_21_continue: /* CIL Label */ ;
      {
#line 164
      __cil_tmp2 = (unsigned int )dll;
#line 164
      __cil_tmp3 = __cil_tmp2 + 8;
#line 164
      __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
#line 164
      if (! __cil_tmp4) {
        {
#line 164
        fail();
        }
      } else {

      }
      }
      goto while_21_break;
    }
    while_21_break: /* CIL Label */ ;
    }
#line 163
    dll = *((struct master_item **)dll);
  }
  while_20_break: /* CIL Label */ ;
  }
#line 165
  return;
}
}
#line 167 "dll_of_dll_BUG.c"
void inspect_init(struct master_item *dll ) 
{ unsigned int __cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  struct slave_item *__cil_tmp4 ;
  int __cil_tmp5 ;

  {
  {
#line 169
  inspect_base(dll);
  }
  {
#line 171
  while (1) {
    while_22_continue: /* CIL Label */ ;
#line 171
    if (dll) {

    } else {
      goto while_22_break;
    }
    {
#line 172
    while (1) {
      while_23_continue: /* CIL Label */ ;
      {
#line 172
      __cil_tmp2 = (unsigned int )dll;
#line 172
      __cil_tmp3 = __cil_tmp2 + 8;
#line 172
      __cil_tmp4 = *((struct slave_item **)__cil_tmp3);
#line 172
      __cil_tmp5 = ! __cil_tmp4;
#line 172
      if (! __cil_tmp5) {
        {
#line 172
        fail();
        }
      } else {

      }
      }
      goto while_23_break;
    }
    while_23_break: /* CIL Label */ ;
    }
#line 171
    dll = *((struct master_item **)dll);
  }
  while_22_break: /* CIL Label */ ;
  }
#line 173
  return;
}
}
#line 175 "dll_of_dll_BUG.c"
int main(void) 
{ struct master_item *dll ;
  struct master_item *tmp ;

  {
  {
#line 177
  tmp = dll_create_master();
#line 177
  dll = tmp;
#line 178
  inspect_full(dll);
#line 180
  dll_destroy_nested_lists(dll);
#line 181
  inspect_dangling(dll);
#line 183
  dll_reinit_nested_lists(dll);
#line 184
  inspect_init(dll);
#line 187
  dll_destroy_master(dll);
  }
#line 188
  return (0);
}
}