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 19 "sll_to_dll_rev_BUG.c"
  struct node {
     struct node *next ;
     struct node *prev ;
 };
 #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 "sll_to_dll_rev_BUG.c"
 extern int __VERIFIER_nondet_int(void) ;
 #line 5 "sll_to_dll_rev_BUG.c"
 static void fail(void) 
 { 
 
   {
   ERROR: 
   goto ERROR;
 }
 }
 #line 24 "sll_to_dll_rev_BUG.c"
 static struct node *alloc_node(void) 
 { struct node *ptr ;
   void *tmp ;
   unsigned int __cil_tmp3 ;
   void *__cil_tmp4 ;
   unsigned int __cil_tmp5 ;
   unsigned int __cil_tmp6 ;
   void *__cil_tmp7 ;
 
   {
   {
 #line 26
   __cil_tmp3 = (unsigned int )8UL;
 #line 26
   tmp = malloc(__cil_tmp3);
 #line 26
   ptr = (struct node *)tmp;
   }
 #line 27
   if (! ptr) {
     {
 #line 28
     abort();
     }
   } else {
 
   }
 #line 30
   __cil_tmp4 = (void *)0;
 #line 30
   *((struct node **)ptr) = (struct node *)__cil_tmp4;
 #line 31
   __cil_tmp5 = (unsigned int )ptr;
 #line 31
   __cil_tmp6 = __cil_tmp5 + 4;
 #line 31
   __cil_tmp7 = (void *)0;
 #line 31
   *((struct node **)__cil_tmp6) = (struct node *)__cil_tmp7;
 #line 32
   return (ptr);
 }
 }
 #line 35 "sll_to_dll_rev_BUG.c"
 static void chain_node(struct node **ppnode ) 
 { struct node *node ;
   struct node *tmp ;
 
   {
   {
 #line 37
   tmp = alloc_node();
 #line 37
   node = tmp;
 #line 38
   *((struct node **)node) = *ppnode;
 #line 39
   *ppnode = node;
   }
 #line 40
   return;
 }
 }
 #line 42 "sll_to_dll_rev_BUG.c"
 static struct node *create_sll(struct node  const  **pp1 , struct node  const  **pp2 ) 
 { struct node *list ;
   int tmp ;
   int tmp___0 ;
   int tmp___1 ;
   struct node **__cil_tmp7 ;
   void *__cil_tmp8 ;
  struct node **__cil_tmp9 ;
  struct node *__cil_tmp10 ;
  struct node **__cil_tmp11 ;
  struct node *__cil_tmp12 ;
  struct node **__cil_tmp13 ;

  {
#line 44
  __cil_tmp7 = & list;
#line 44
  __cil_tmp8 = (void *)0;
#line 44
  *__cil_tmp7 = (struct node *)__cil_tmp8;
  {
#line 46
  while (1) {
    while_0_continue: /* CIL Label */ ;
    {
#line 47
    chain_node(& list);
#line 46
    tmp = __VERIFIER_nondet_int();
    }
#line 46
    if (tmp) {

    } else {
      goto while_0_break;
    }
  }
  while_0_break: /* CIL Label */ ;
  }
#line 50
  __cil_tmp9 = & list;
#line 50
  __cil_tmp10 = *__cil_tmp9;
#line 50
  *pp2 = (struct node  const  *)__cil_tmp10;
  {
#line 52
  while (1) {
    while_1_continue: /* CIL Label */ ;
    {
#line 52
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 52
    if (tmp___0) {

    } else {
      goto while_1_break;
    }
    {
#line 53
    chain_node(& list);
    }
  }
  while_1_break: /* CIL Label */ ;
  }
#line 55
  __cil_tmp11 = & list;
#line 55
  __cil_tmp12 = *__cil_tmp11;
#line 55
  *pp1 = (struct node  const  *)__cil_tmp12;
  {
#line 57
  while (1) {
    while_2_continue: /* CIL Label */ ;
    {
#line 58
    chain_node(& list);
#line 57
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 57
    if (tmp___1) {

    } else {
      goto while_2_break;
    }
  }
  while_2_break: /* CIL Label */ ;
  }
  {
#line 61
  __cil_tmp13 = & list;
#line 61
  return (*__cil_tmp13);
  }
}
}
#line 64 "sll_to_dll_rev_BUG.c"
void init_back_link(struct node *list ) 
{ struct node *next ;
  unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;

  {
  {
#line 65
  while (1) {
    while_3_continue: /* CIL Label */ ;
#line 66
    next = *((struct node **)list);
#line 67
    if (! next) {
#line 68
      return;
    } else {

    }
#line 70
    __cil_tmp3 = (unsigned int )next;
#line 70
    __cil_tmp4 = __cil_tmp3 + 4;
#line 70
    *((struct node **)__cil_tmp4) = list;
#line 71
    list = next;
  }
  while_3_break: /* CIL Label */ ;
  }
}
}
#line 75 "sll_to_dll_rev_BUG.c"
void reverse_dll(struct node *list ) 
{ struct node *next ;
  unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  unsigned int __cil_tmp5 ;
  unsigned int __cil_tmp6 ;

  {
  {
#line 76
  while (1) {
    while_4_continue: /* CIL Label */ ;
#line 76
    if (list) {

    } else {
      goto while_4_break;
    }
#line 77
    next = *((struct node **)list);
#line 78
    __cil_tmp3 = (unsigned int )list;
#line 78
    __cil_tmp4 = __cil_tmp3 + 4;
#line 78
    *((struct node **)list) = *((struct node **)__cil_tmp4);
#line 79
    __cil_tmp5 = (unsigned int )list;
#line 79
    __cil_tmp6 = __cil_tmp5 + 4;
#line 79
    *((struct node **)__cil_tmp6) = next;
#line 80
    list = next;
  }
  while_4_break: /* CIL Label */ ;
  }
#line 82
  return;
}
}
#line 84 "sll_to_dll_rev_BUG.c"
void remove_fw_link(struct node *list ) 
{ struct node *next ;
  void *__cil_tmp3 ;

  {
  {
#line 85
  while (1) {
    while_5_continue: /* CIL Label */ ;
#line 85
    if (list) {

    } else {
      goto while_5_break;
    }
#line 86
    next = *((struct node **)list);
#line 87
    __cil_tmp3 = (void *)0;
#line 87
    *((struct node **)list) = (struct node *)__cil_tmp3;
#line 88
    list = next;
  }
  while_5_break: /* CIL Label */ ;
  }
#line 90
  return;
}
}
#line 92 "sll_to_dll_rev_BUG.c"
void check_seq_next(struct node  const  *beg , struct node  const  *end ) 
{ struct node *__cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  unsigned int __cil_tmp5 ;
  struct node *__cil_tmp6 ;

  {
  {
#line 93
  while (1) {
    while_6_continue: /* CIL Label */ ;
#line 93
    if (! beg) {
      {
#line 93
      fail();
      }
    } else {

    }
    goto while_6_break;
  }
  while_6_break: /* CIL Label */ ;
  }
  {
#line 94
  while (1) {
    while_7_continue: /* CIL Label */ ;
#line 94
    if (! end) {
      {
#line 94
      fail();
      }
    } else {

    }
    goto while_7_break;
  }
  while_7_break: /* CIL Label */ ;
  }
#line 96
  __cil_tmp3 = *((struct node * const  *)beg);
#line 96
  beg = (struct node  const  *)__cil_tmp3;
  {
#line 96
  while (1) {
    while_8_continue: /* CIL Label */ ;
    {
#line 96
    __cil_tmp4 = (unsigned int )beg;
#line 96
    __cil_tmp5 = (unsigned int )end;
#line 96
    if (__cil_tmp5 != __cil_tmp4) {

    } else {
      goto while_8_break;
    }
    }
    {
#line 97
    while (1) {
      while_9_continue: /* CIL Label */ ;
#line 97
      if (! beg) {
        {
#line 97
        fail();
        }
      } else {

      }
      goto while_9_break;
    }
    while_9_break: /* CIL Label */ ;
    }
#line 96
    __cil_tmp6 = *((struct node * const  *)beg);
#line 96
    beg = (struct node  const  *)__cil_tmp6;
  }
  while_8_break: /* CIL Label */ ;
  }
#line 98
  return;
}
}
#line 100 "sll_to_dll_rev_BUG.c"
void check_seq_prev(struct node  const  *beg , struct node  const  *end ) 
{ unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  struct node *__cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  unsigned int __cil_tmp9 ;
  struct node *__cil_tmp10 ;

  {
  {
#line 101
  while (1) {
    while_10_continue: /* CIL Label */ ;
#line 101
    if (! beg) {
      {
#line 101
      fail();
      }
    } else {

    }
    goto while_10_break;
  }
  while_10_break: /* CIL Label */ ;
  }
  {
#line 102
  while (1) {
    while_11_continue: /* CIL Label */ ;
#line 102
    if (! end) {
      {
#line 102
      fail();
      }
    } else {

    }
    goto while_11_break;
  }
  while_11_break: /* CIL Label */ ;
  }
#line 104
  __cil_tmp3 = (unsigned int )beg;
#line 104
  __cil_tmp4 = __cil_tmp3 + 4;
#line 104
  __cil_tmp5 = *((struct node * const  *)__cil_tmp4);
#line 104
  beg = (struct node  const  *)__cil_tmp5;
  {
#line 104
  while (1) {
    while_12_continue: /* CIL Label */ ;
    {
#line 104
    __cil_tmp6 = (unsigned int )beg;
#line 104
    __cil_tmp7 = (unsigned int )end;
#line 104
    if (__cil_tmp7 != __cil_tmp6) {

    } else {
      goto while_12_break;
    }
    }
    {
#line 105
    while (1) {
      while_13_continue: /* CIL Label */ ;
#line 105
      if (! beg) {
        {
#line 105
        fail();
        }
      } else {

      }
      goto while_13_break;
    }
    while_13_break: /* CIL Label */ ;
    }
#line 104
    __cil_tmp8 = (unsigned int )beg;
#line 104
    __cil_tmp9 = __cil_tmp8 + 4;
#line 104
    __cil_tmp10 = *((struct node * const  *)__cil_tmp9);
#line 104
    beg = (struct node  const  *)__cil_tmp10;
  }
  while_12_break: /* CIL Label */ ;
  }
#line 106
  return;
}
}
#line 108 "sll_to_dll_rev_BUG.c"
int main(void) 
{ struct node  const  *p1 ;
  struct node  const  *p2 ;
  struct node *list ;
  struct node *tmp ;
  struct node *prev ;
  struct node  const  **__cil_tmp6 ;
  struct node  const  *__cil_tmp7 ;
  struct node  const  **__cil_tmp8 ;
  struct node  const  *__cil_tmp9 ;
  struct node  const  **__cil_tmp10 ;
  struct node  const  *__cil_tmp11 ;
  unsigned int __cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  struct node *__cil_tmp14 ;
  int __cil_tmp15 ;
  struct node  const  **__cil_tmp16 ;
  struct node  const  *__cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  struct node *__cil_tmp20 ;
  int __cil_tmp21 ;
  struct node  const  **__cil_tmp22 ;
  struct node  const  *__cil_tmp23 ;
  struct node  const  **__cil_tmp24 ;
  struct node  const  *__cil_tmp25 ;
  struct node  const  **__cil_tmp26 ;
  struct node  const  *__cil_tmp27 ;
  struct node  const  **__cil_tmp28 ;
  struct node  const  *__cil_tmp29 ;
  struct node  const  **__cil_tmp30 ;
  struct node  const  *__cil_tmp31 ;
  struct node  const  **__cil_tmp32 ;
  struct node  const  *__cil_tmp33 ;
  struct node  const  **__cil_tmp34 ;
  struct node  const  *__cil_tmp35 ;
  struct node  const  **__cil_tmp36 ;
  struct node  const  *__cil_tmp37 ;
  struct node  const  **__cil_tmp38 ;
  struct node  const  *__cil_tmp39 ;
  struct node  const  **__cil_tmp40 ;
  struct node  const  *__cil_tmp41 ;
  unsigned int __cil_tmp42 ;
  unsigned int __cil_tmp43 ;
  void *__cil_tmp44 ;

  {
  {
#line 112
  tmp = create_sll(& p1, & p2);
#line 112
  list = tmp;
  }
  {
#line 113
  while (1) {
    while_14_continue: /* CIL Label */ ;
    goto while_14_break;
  }
  while_14_break: /* CIL Label */ ;
  }
  {
#line 114
  __cil_tmp6 = & p1;
#line 114
  __cil_tmp7 = *__cil_tmp6;
#line 114
  __cil_tmp8 = & p2;
#line 114
  __cil_tmp9 = *__cil_tmp8;
#line 114
  check_seq_next(__cil_tmp7, __cil_tmp9);
  }
  {
#line 115
  while (1) {
    while_15_continue: /* CIL Label */ ;
    {
#line 115
    __cil_tmp10 = & p1;
#line 115
    __cil_tmp11 = *__cil_tmp10;
#line 115
    __cil_tmp12 = (unsigned int )__cil_tmp11;
#line 115
    __cil_tmp13 = __cil_tmp12 + 4;
#line 115
    __cil_tmp14 = *((struct node * const  *)__cil_tmp13);
#line 115
    __cil_tmp15 = ! __cil_tmp14;
#line 115
    if (! __cil_tmp15) {
      {
#line 115
      fail();
      }
    } else {

    }
    }
    goto while_15_break;
  }
  while_15_break: /* CIL Label */ ;
  }
  {
#line 116
  while (1) {
    while_16_continue: /* CIL Label */ ;
    {
#line 116
    __cil_tmp16 = & p2;
#line 116
    __cil_tmp17 = *__cil_tmp16;
#line 116
    __cil_tmp18 = (unsigned int )__cil_tmp17;
#line 116
    __cil_tmp19 = __cil_tmp18 + 4;
#line 116
    __cil_tmp20 = *((struct node * const  *)__cil_tmp19);
#line 116
    __cil_tmp21 = ! __cil_tmp20;
#line 116
    if (! __cil_tmp21) {
      {
#line 116
      fail();
      }
    } else {

    }
    }
    goto while_16_break;
  }
  while_16_break: /* CIL Label */ ;
  }
  {
#line 118
  init_back_link(list);
  }
  {
#line 119
  while (1) {
    while_17_continue: /* CIL Label */ ;
    goto while_17_break;
  }
  while_17_break: /* CIL Label */ ;
  }
  {
#line 120
  __cil_tmp22 = & p1;
#line 120
  __cil_tmp23 = *__cil_tmp22;
#line 120
  __cil_tmp24 = & p2;
#line 120
  __cil_tmp25 = *__cil_tmp24;
#line 120
  check_seq_next(__cil_tmp23, __cil_tmp25);
#line 121
  __cil_tmp26 = & p2;
#line 121
  __cil_tmp27 = *__cil_tmp26;
#line 121
  __cil_tmp28 = & p1;
#line 121
  __cil_tmp29 = *__cil_tmp28;
#line 121
  check_seq_prev(__cil_tmp27, __cil_tmp29);
#line 123
  reverse_dll(list);
  }
  {
#line 124
  while (1) {
    while_18_continue: /* CIL Label */ ;
    goto while_18_break;
  }
  while_18_break: /* CIL Label */ ;
  }
  {
#line 125
  __cil_tmp30 = & p1;
#line 125
  __cil_tmp31 = *__cil_tmp30;
#line 125
  __cil_tmp32 = & p2;
#line 125
  __cil_tmp33 = *__cil_tmp32;
#line 125
  check_seq_prev(__cil_tmp31, __cil_tmp33);
#line 126
  __cil_tmp34 = & p2;
#line 126
  __cil_tmp35 = *__cil_tmp34;
#line 126
  __cil_tmp36 = & p1;
#line 126
  __cil_tmp37 = *__cil_tmp36;
#line 126
  check_seq_next(__cil_tmp35, __cil_tmp37);
#line 128
  remove_fw_link(list);
  }
  {
#line 129
  while (1) {
    while_19_continue: /* CIL Label */ ;
    goto while_19_break;
  }
  while_19_break: /* CIL Label */ ;
  }
  {
#line 130
  __cil_tmp38 = & p1;
#line 130
  __cil_tmp39 = *__cil_tmp38;
#line 130
  __cil_tmp40 = & p2;
#line 130
  __cil_tmp41 = *__cil_tmp40;
#line 130
  check_seq_prev(__cil_tmp39, __cil_tmp41);
  }
  {
#line 132
  while (1) {
    while_20_continue: /* CIL Label */ ;
#line 132
    if (list) {

    } else {
      goto while_20_break;
    }
    {
#line 133
    __cil_tmp42 = (unsigned int )list;
#line 133
    __cil_tmp43 = __cil_tmp42 + 4;
#line 133
    prev = *((struct node **)__cil_tmp43);
#line 134
    __cil_tmp44 = (void *)list;
#line 134
    free(__cil_tmp44);
#line 135
    list = prev;
    }
  }
  while_20_break: /* CIL Label */ ;
  }
#line 138
  return (0);
}
}