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.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.c"
 extern int __VERIFIER_nondet_int(void) ;
 #line 5 "sll_to_dll_rev.c"
 static void fail(void) 
 { 
 
   {
   ERROR: 
   goto ERROR;
 }
 }
 #line 24 "sll_to_dll_rev.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.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.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 53
    chain_node(& list);
#line 52
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 52
    if (tmp___0) {

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

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

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

    }
#line 71
    __cil_tmp3 = (unsigned int )next;
#line 71
    __cil_tmp4 = __cil_tmp3 + 4;
#line 71
    *((struct node **)__cil_tmp4) = list;
#line 72
    list = next;
  }
  while_3_break: /* CIL Label */ ;
  }
}
}
#line 76 "sll_to_dll_rev.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 77
  while (1) {
    while_4_continue: /* CIL Label */ ;
#line 77
    if (list) {

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

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

    } else {
      goto while_5_break;
    }
#line 87
    next = *((struct node **)list);
#line 88
    __cil_tmp3 = (void *)0;
#line 88
    *((struct node **)list) = (struct node *)__cil_tmp3;
#line 89
    list = next;
  }
  while_5_break: /* CIL Label */ ;
  }
#line 91
  return;
}
}
#line 93 "sll_to_dll_rev.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 94
  while (1) {
    while_6_continue: /* CIL Label */ ;
#line 94
    if (! beg) {
      {
#line 94
      fail();
      }
    } else {

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

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

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

      }
      goto while_9_break;
    }
    while_9_break: /* CIL Label */ ;
    }
#line 97
    __cil_tmp6 = *((struct node * const  *)beg);
#line 97
    beg = (struct node  const  *)__cil_tmp6;
  }
  while_8_break: /* CIL Label */ ;
  }
#line 99
  return;
}
}
#line 101 "sll_to_dll_rev.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 102
  while (1) {
    while_10_continue: /* CIL Label */ ;
#line 102
    if (! beg) {
      {
#line 102
      fail();
      }
    } else {

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

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

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

      }
      goto while_13_break;
    }
    while_13_break: /* CIL Label */ ;
    }
#line 105
    __cil_tmp8 = (unsigned int )beg;
#line 105
    __cil_tmp9 = __cil_tmp8 + 4;
#line 105
    __cil_tmp10 = *((struct node * const  *)__cil_tmp9);
#line 105
    beg = (struct node  const  *)__cil_tmp10;
  }
  while_12_break: /* CIL Label */ ;
  }
#line 107
  return;
}
}
#line 109 "sll_to_dll_rev.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 113
  tmp = create_sll(& p1, & p2);
#line 113
  list = tmp;
  }
  {
#line 114
  while (1) {
    while_14_continue: /* CIL Label */ ;
    goto while_14_break;
  }
  while_14_break: /* CIL Label */ ;
  }
  {
#line 115
  __cil_tmp6 = & p1;
#line 115
  __cil_tmp7 = *__cil_tmp6;
#line 115
  __cil_tmp8 = & p2;
#line 115
  __cil_tmp9 = *__cil_tmp8;
#line 115
  check_seq_next(__cil_tmp7, __cil_tmp9);
  }
  {
#line 116
  while (1) {
    while_15_continue: /* CIL Label */ ;
    {
#line 116
    __cil_tmp10 = & p1;
#line 116
    __cil_tmp11 = *__cil_tmp10;
#line 116
    __cil_tmp12 = (unsigned int )__cil_tmp11;
#line 116
    __cil_tmp13 = __cil_tmp12 + 4;
#line 116
    __cil_tmp14 = *((struct node * const  *)__cil_tmp13);
#line 116
    __cil_tmp15 = ! __cil_tmp14;
#line 116
    if (! __cil_tmp15) {
      {
#line 116
      fail();
      }
    } else {

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

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

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