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 "test-0177.c"
  struct node {
     struct node *next ;
     int value ;
 };
 #line 20 "test-0177.c"
 struct list {
    struct node *slist ;
    struct list *next ;
 };
 #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 "test-0177.c"
 extern int __VERIFIER_nondet_int(void) ;
 #line 5 "test-0177.c"
 static void fail(void) 
 { 
 
   {
   ERROR: 
   goto ERROR;
 }
 }
 #line 25 "test-0177.c"
 static void merge_single_node(struct node ***dst , struct node **data ) 
 { struct node *node ;
   void *__cil_tmp4 ;
   struct node **__cil_tmp5 ;
 
   {
 #line 29
   node = *data;
 #line 30
   *data = *((struct node **)node);
 #line 31
   __cil_tmp4 = (void *)0;
 #line 31
   *((struct node **)node) = (struct node *)__cil_tmp4;
 #line 34
   __cil_tmp5 = *dst;
 #line 34
   *__cil_tmp5 = node;
 #line 35
   *dst = (struct node **)node;
 #line 36
   return;
 }
 }
 #line 38 "test-0177.c"
 static void merge_pair(struct node **dst , struct node *sub1 , struct node *sub2 ) 
 { struct node **__cil_tmp4 ;
   struct node **__cil_tmp5 ;
   struct node **__cil_tmp6 ;
   struct node *__cil_tmp7 ;
   struct node **__cil_tmp8 ;
   struct node **__cil_tmp9 ;
   struct node *__cil_tmp10 ;
   unsigned int __cil_tmp11 ;
   unsigned int __cil_tmp12 ;
   int __cil_tmp13 ;
   struct node **__cil_tmp14 ;
   struct node *__cil_tmp15 ;
   unsigned int __cil_tmp16 ;
   unsigned int __cil_tmp17 ;
   int __cil_tmp18 ;
 
   {
   {
 #line 43
   while (1) {
     while_0_continue: /* CIL Label */ ;
     {
 #line 43
     __cil_tmp4 = & sub1;
 #line 43
     if (*__cil_tmp4) {
 
     } else {
       {
 #line 43
       __cil_tmp5 = & sub2;
 #line 43
       if (*__cil_tmp5) {
 
       } else {
         goto while_0_break;
       }
       }
     }
     }
    {
#line 44
    __cil_tmp6 = & sub2;
#line 44
    __cil_tmp7 = *__cil_tmp6;
#line 44
    if (! __cil_tmp7) {
      {
#line 45
      merge_single_node(& dst, & sub1);
      }
    } else {
      {
#line 44
      __cil_tmp8 = & sub1;
#line 44
      if (*__cil_tmp8) {
        {
#line 44
        __cil_tmp9 = & sub2;
#line 44
        __cil_tmp10 = *__cil_tmp9;
#line 44
        __cil_tmp11 = (unsigned int )__cil_tmp10;
#line 44
        __cil_tmp12 = __cil_tmp11 + 4;
#line 44
        __cil_tmp13 = *((int *)__cil_tmp12);
#line 44
        __cil_tmp14 = & sub1;
#line 44
        __cil_tmp15 = *__cil_tmp14;
#line 44
        __cil_tmp16 = (unsigned int )__cil_tmp15;
#line 44
        __cil_tmp17 = __cil_tmp16 + 4;
#line 44
        __cil_tmp18 = *((int *)__cil_tmp17);
#line 44
        if (__cil_tmp18 < __cil_tmp13) {
          {
#line 45
          merge_single_node(& dst, & sub1);
          }
        } else {
          {
#line 47
          merge_single_node(& dst, & sub2);
          }
        }
        }
      } else {
        {
#line 47
        merge_single_node(& dst, & sub2);
        }
      }
      }
    }
    }
  }
  while_0_break: /* CIL Label */ ;
  }
#line 49
  return;
}
}
#line 51 "test-0177.c"
static struct list *seq_sort_core(struct list *data ) 
{ struct list *dst ;
  struct list *next ;
  void *__cil_tmp4 ;
  unsigned int __cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  struct node **__cil_tmp9 ;
  struct node *__cil_tmp10 ;
  struct node *__cil_tmp11 ;
  unsigned int __cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  void *__cil_tmp16 ;

  {
#line 53
  __cil_tmp4 = (void *)0;
#line 53
  dst = (struct list *)__cil_tmp4;
  {
#line 55
  while (1) {
    while_1_continue: /* CIL Label */ ;
#line 55
    if (data) {

    } else {
      goto while_1_break;
    }
#line 56
    __cil_tmp5 = (unsigned int )data;
#line 56
    __cil_tmp6 = __cil_tmp5 + 4;
#line 56
    next = *((struct list **)__cil_tmp6);
#line 57
    if (! next) {
#line 59
      __cil_tmp7 = (unsigned int )data;
#line 59
      __cil_tmp8 = __cil_tmp7 + 4;
#line 59
      *((struct list **)__cil_tmp8) = dst;
#line 60
      dst = data;
      goto while_1_break;
    } else {

    }
    {
#line 65
    __cil_tmp9 = (struct node **)data;
#line 65
    __cil_tmp10 = *((struct node **)data);
#line 65
    __cil_tmp11 = *((struct node **)next);
#line 65
    merge_pair(__cil_tmp9, __cil_tmp10, __cil_tmp11);
#line 66
    __cil_tmp12 = (unsigned int )data;
#line 66
    __cil_tmp13 = __cil_tmp12 + 4;
#line 66
    *((struct list **)__cil_tmp13) = dst;
#line 67
    dst = data;
#line 70
    __cil_tmp14 = (unsigned int )next;
#line 70
    __cil_tmp15 = __cil_tmp14 + 4;
#line 70
    data = *((struct list **)__cil_tmp15);
#line 71
    __cil_tmp16 = (void *)next;
#line 71
    free(__cil_tmp16);
    }
  }
  while_1_break: /* CIL Label */ ;
  }
#line 74
  return (dst);
}
}
#line 77 "test-0177.c"
static void inspect_before(struct list *shape ) 
{ unsigned int __cil_tmp2 ;
  unsigned int __cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  unsigned int __cil_tmp5 ;
  struct list *__cil_tmp6 ;
  struct node *__cil_tmp7 ;
  void *__cil_tmp8 ;
  unsigned int __cil_tmp9 ;
  struct node *__cil_tmp10 ;
  struct node *__cil_tmp11 ;
  unsigned int __cil_tmp12 ;
  int __cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  void *__cil_tmp16 ;
  unsigned int __cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  unsigned int __cil_tmp19 ;
  struct list *__cil_tmp20 ;
  unsigned int __cil_tmp21 ;
  int __cil_tmp22 ;
  struct node *__cil_tmp23 ;
  void *__cil_tmp24 ;
  unsigned int __cil_tmp25 ;
  struct node *__cil_tmp26 ;
  struct node *__cil_tmp27 ;
  unsigned int __cil_tmp28 ;
  int __cil_tmp29 ;

  {
  {
#line 80
  while (1) {
    while_2_continue: /* CIL Label */ ;
#line 80
    if (! shape) {
      {
#line 80
      fail();
      }
    } else {

    }
    goto while_2_break;
  }
  while_2_break: /* CIL Label */ ;
  }
  {
#line 82
  while (1) {
    while_3_continue: /* CIL Label */ ;
    {
#line 82
    __cil_tmp2 = (unsigned int )shape;
#line 82
    __cil_tmp3 = __cil_tmp2 + 4;
#line 82
    if (*((struct list **)__cil_tmp3)) {

    } else {
      goto while_3_break;
    }
    }
    {
#line 83
    while (1) {
      while_4_continue: /* CIL Label */ ;
#line 83
      if (! shape) {
        {
#line 83
        fail();
        }
      } else {

      }
      goto while_4_break;
    }
    while_4_break: /* CIL Label */ ;
    }
    {
#line 84
    while (1) {
      while_5_continue: /* CIL Label */ ;
      {
#line 84
      __cil_tmp4 = (unsigned int )shape;
#line 84
      __cil_tmp5 = __cil_tmp4 + 4;
#line 84
      __cil_tmp6 = *((struct list **)__cil_tmp5);
#line 84
      if (! __cil_tmp6) {
        {
#line 84
        fail();
        }
      } else {

      }
      }
      goto while_5_break;
    }
    while_5_break: /* CIL Label */ ;
    }
    {
#line 85
    while (1) {
      while_6_continue: /* CIL Label */ ;
      {
#line 85
      __cil_tmp7 = *((struct node **)shape);
#line 85
      if (! __cil_tmp7) {
        {
#line 85
        fail();
        }
      } else {

      }
      }
      goto while_6_break;
    }
    while_6_break: /* CIL Label */ ;
    }
    {
#line 86
    while (1) {
      while_7_continue: /* CIL Label */ ;
      {
#line 86
      __cil_tmp8 = (void *)0;
#line 86
      __cil_tmp9 = (unsigned int )__cil_tmp8;
#line 86
      __cil_tmp10 = *((struct node **)shape);
#line 86
      __cil_tmp11 = *((struct node **)__cil_tmp10);
#line 86
      __cil_tmp12 = (unsigned int )__cil_tmp11;
#line 86
      __cil_tmp13 = __cil_tmp12 == __cil_tmp9;
#line 86
      if (! __cil_tmp13) {
        {
#line 86
        fail();
        }
      } else {

      }
      }
      goto while_7_break;
    }
    while_7_break: /* CIL Label */ ;
    }
#line 82
    __cil_tmp14 = (unsigned int )shape;
#line 82
    __cil_tmp15 = __cil_tmp14 + 4;
#line 82
    shape = *((struct list **)__cil_tmp15);
  }
  while_3_break: /* CIL Label */ ;
  }
  {
#line 90
  while (1) {
    while_8_continue: /* CIL Label */ ;
#line 90
    if (! shape) {
      {
#line 90
      fail();
      }
    } else {

    }
    goto while_8_break;
  }
  while_8_break: /* CIL Label */ ;
  }
  {
#line 91
  while (1) {
    while_9_continue: /* CIL Label */ ;
    {
#line 91
    __cil_tmp16 = (void *)0;
#line 91
    __cil_tmp17 = (unsigned int )__cil_tmp16;
#line 91
    __cil_tmp18 = (unsigned int )shape;
#line 91
    __cil_tmp19 = __cil_tmp18 + 4;
#line 91
    __cil_tmp20 = *((struct list **)__cil_tmp19);
#line 91
    __cil_tmp21 = (unsigned int )__cil_tmp20;
#line 91
    __cil_tmp22 = __cil_tmp21 == __cil_tmp17;
#line 91
    if (! __cil_tmp22) {
      {
#line 91
      fail();
      }
    } else {

    }
    }
    goto while_9_break;
  }
  while_9_break: /* CIL Label */ ;
  }
  {
#line 92
  while (1) {
    while_10_continue: /* CIL Label */ ;
    {
#line 92
    __cil_tmp23 = *((struct node **)shape);
#line 92
    if (! __cil_tmp23) {
      {
#line 92
      fail();
      }
    } else {

    }
    }
    goto while_10_break;
  }
  while_10_break: /* CIL Label */ ;
  }
  {
#line 93
  while (1) {
    while_11_continue: /* CIL Label */ ;
    {
#line 93
    __cil_tmp24 = (void *)0;
#line 93
    __cil_tmp25 = (unsigned int )__cil_tmp24;
#line 93
    __cil_tmp26 = *((struct node **)shape);
#line 93
    __cil_tmp27 = *((struct node **)__cil_tmp26);
#line 93
    __cil_tmp28 = (unsigned int )__cil_tmp27;
#line 93
    __cil_tmp29 = __cil_tmp28 == __cil_tmp25;
#line 93
    if (! __cil_tmp29) {
      {
#line 93
      fail();
      }
    } else {

    }
    }
    goto while_11_break;
  }
  while_11_break: /* CIL Label */ ;
  }
#line 94
  return;
}
}
#line 96 "test-0177.c"
static void inspect_after(struct list *shape ) 
{ struct node *pos ;
  void *__cil_tmp3 ;
  unsigned int __cil_tmp4 ;
  unsigned int __cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  struct list *__cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  int __cil_tmp9 ;
  void *__cil_tmp10 ;
  unsigned int __cil_tmp11 ;
  struct node *__cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  int __cil_tmp14 ;
  struct node *__cil_tmp15 ;
  int __cil_tmp16 ;

  {
  {
#line 99
  while (1) {
    while_12_continue: /* CIL Label */ ;
#line 99
    if (! shape) {
      {
#line 99
      fail();
      }
    } else {

    }
    goto while_12_break;
  }
  while_12_break: /* CIL Label */ ;
  }
  {
#line 100
  while (1) {
    while_13_continue: /* CIL Label */ ;
    {
#line 100
    __cil_tmp3 = (void *)0;
#line 100
    __cil_tmp4 = (unsigned int )__cil_tmp3;
#line 100
    __cil_tmp5 = (unsigned int )shape;
#line 100
    __cil_tmp6 = __cil_tmp5 + 4;
#line 100
    __cil_tmp7 = *((struct list **)__cil_tmp6);
#line 100
    __cil_tmp8 = (unsigned int )__cil_tmp7;
#line 100
    __cil_tmp9 = __cil_tmp8 == __cil_tmp4;
#line 100
    if (! __cil_tmp9) {
      {
#line 100
      fail();
      }
    } else {

    }
    }
    goto while_13_break;
  }
  while_13_break: /* CIL Label */ ;
  }
  {
#line 101
  while (1) {
    while_14_continue: /* CIL Label */ ;
    {
#line 101
    __cil_tmp10 = (void *)0;
#line 101
    __cil_tmp11 = (unsigned int )__cil_tmp10;
#line 101
    __cil_tmp12 = *((struct node **)shape);
#line 101
    __cil_tmp13 = (unsigned int )__cil_tmp12;
#line 101
    __cil_tmp14 = __cil_tmp13 != __cil_tmp11;
#line 101
    if (! __cil_tmp14) {
      {
#line 101
      fail();
      }
    } else {

    }
    }
    goto while_14_break;
  }
  while_14_break: /* CIL Label */ ;
  }
#line 105
  pos = *((struct node **)shape);
  {
#line 105
  while (1) {
    while_15_continue: /* CIL Label */ ;
#line 105
    if (*((struct node **)pos)) {

    } else {
      goto while_15_break;
    }
#line 105
    pos = *((struct node **)pos);
  }
  while_15_break: /* CIL Label */ ;
  }
  {
#line 106
  while (1) {
    while_16_continue: /* CIL Label */ ;
    {
#line 106
    __cil_tmp15 = *((struct node **)pos);
#line 106
    __cil_tmp16 = ! __cil_tmp15;
#line 106
    if (! __cil_tmp16) {
      {
#line 106
      fail();
      }
    } else {

    }
    }
    goto while_16_break;
  }
  while_16_break: /* CIL Label */ ;
  }
#line 107
  return;
}
}
#line 109 "test-0177.c"
int main(void) 
{ struct list *data ;
  struct node *node ;
  void *tmp ;
  struct list *item ;
  void *tmp___0 ;
  int tmp___1 ;
  struct node *node___0 ;
  struct node *snext ;
  void *__cil_tmp9 ;
  unsigned int __cil_tmp10 ;
  void *__cil_tmp11 ;
  unsigned int __cil_tmp12 ;
  unsigned int __cil_tmp13 ;
  unsigned int __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  unsigned int __cil_tmp16 ;
  unsigned int __cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  void *__cil_tmp19 ;
  void *__cil_tmp20 ;

  {
#line 111
  __cil_tmp9 = (void *)0;
#line 111
  data = (struct list *)__cil_tmp9;
  {
#line 112
  while (1) {
    while_17_continue: /* CIL Label */ ;
    {
#line 112
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 112
    if (tmp___1) {

    } else {
      goto while_17_break;
    }
    {
#line 113
    __cil_tmp10 = (unsigned int )8UL;
#line 113
    tmp = malloc(__cil_tmp10);
#line 113
    node = (struct node *)tmp;
    }
#line 114
    if (! node) {
      {
#line 115
      abort();
      }
    } else {

    }
    {
#line 117
    __cil_tmp11 = (void *)0;
#line 117
    *((struct node **)node) = (struct node *)__cil_tmp11;
#line 118
    __cil_tmp12 = (unsigned int )node;
#line 118
    __cil_tmp13 = __cil_tmp12 + 4;
#line 118
    *((int *)__cil_tmp13) = __VERIFIER_nondet_int();
#line 120
    __cil_tmp14 = (unsigned int )8UL;
#line 120
    tmp___0 = malloc(__cil_tmp14);
#line 120
    item = (struct list *)tmp___0;
    }
#line 121
    if (! item) {
      {
#line 122
      abort();
      }
    } else {

    }
#line 124
    *((struct node **)item) = node;
#line 125
    __cil_tmp15 = (unsigned int )item;
#line 125
    __cil_tmp16 = __cil_tmp15 + 4;
#line 125
    *((struct list **)__cil_tmp16) = data;
#line 126
    data = item;
  }
  while_17_break: /* CIL Label */ ;
  }
#line 129
  if (! data) {
#line 130
    return (0);
  } else {

  }
  {
#line 132
  inspect_before(data);
  }
  {
#line 135
  while (1) {
    while_18_continue: /* CIL Label */ ;
    {
#line 135
    __cil_tmp17 = (unsigned int )data;
#line 135
    __cil_tmp18 = __cil_tmp17 + 4;
#line 135
    if (*((struct list **)__cil_tmp18)) {

    } else {
      goto while_18_break;
    }
    }
    {
#line 136
    data = seq_sort_core(data);
    }
  }
  while_18_break: /* CIL Label */ ;
  }
  {
#line 138
  inspect_after(data);
#line 140
  node___0 = *((struct node **)data);
#line 141
  __cil_tmp19 = (void *)data;
#line 141
  free(__cil_tmp19);
  }
  {
#line 143
  while (1) {
    while_19_continue: /* CIL Label */ ;
#line 143
    if (node___0) {

    } else {
      goto while_19_break;
    }
    {
#line 144
    snext = *((struct node **)node___0);
#line 145
    __cil_tmp20 = (void *)node___0;
#line 145
    free(__cil_tmp20);
#line 146
    node___0 = snext;
    }
  }
  while_19_break: /* CIL Label */ ;
  }
#line 149
  return (0);
}
}