ClabureDB: Classified Bug-Reports Database

  extern int __VERIFIER_nondet_int();
  /* Generated by CIL v. 1.3.7 */
  /* print_CIL_Input is true */
  
  #line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
  typedef unsigned long size_t;
  #line 15 "splice.c"
  struct node {
     int h ;
    struct node *n ;
 };
 #line 15 "splice.c"
 typedef struct node *List;
 #line 471 "/usr/include/stdlib.h"
 extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
 #line 544
  __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
 #line 11 "splice.c"
  __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
 #line 11 "splice.c"
 void exit(int s ) 
 { 
 
   {
   _EXIT: 
   goto _EXIT;
 }
 }
 #line 32
 extern int ( /* missing proto */  __VERIFIER_nondet_int)() ;
 #line 20 "splice.c"
 int main(void) 
 { int flag ;
   List a ;
   void *tmp ;
   List t ;
   List l1 ;
   List l2 ;
   List p ;
   void *tmp___0 ;
   int tmp___1 ;
   unsigned long __cil_tmp12 ;
   List __cil_tmp13 ;
   unsigned int __cil_tmp14 ;
   unsigned int __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   List __cil_tmp17 ;
   unsigned int __cil_tmp18 ;
   unsigned int __cil_tmp19 ;
   unsigned int __cil_tmp20 ;
   unsigned int __cil_tmp21 ;
   unsigned int __cil_tmp22 ;
   unsigned int __cil_tmp23 ;
   int __cil_tmp24 ;
   int __cil_tmp25 ;
   unsigned int __cil_tmp26 ;
   unsigned int __cil_tmp27 ;
   unsigned int __cil_tmp28 ;
   unsigned int __cil_tmp29 ;
   unsigned int __cil_tmp30 ;
   unsigned int __cil_tmp31 ;
   List __cil_tmp32 ;
   unsigned int __cil_tmp33 ;
   unsigned int __cil_tmp34 ;
   int __cil_tmp35 ;
   unsigned int __cil_tmp36 ;
   unsigned int __cil_tmp37 ;
   List __cil_tmp38 ;
   unsigned int __cil_tmp39 ;
   unsigned int __cil_tmp40 ;
   int __cil_tmp41 ;
   unsigned int __cil_tmp42 ;
   unsigned int __cil_tmp43 ;
 
   {
   {
 #line 21
   flag = 1;
 #line 24
   __cil_tmp12 = (unsigned long )8U;
 #line 24
   tmp = malloc(__cil_tmp12);
 #line 24
   a = (struct node *)tmp;
   }
   {
 #line 25
   __cil_tmp13 = (List )0;
 #line 25
   __cil_tmp14 = (unsigned int )__cil_tmp13;
 #line 25
   __cil_tmp15 = (unsigned int )a;
 #line 25
   if (__cil_tmp15 == __cil_tmp14) {
     {
 #line 25
     exit(1);
     }
   } else {

  }
  }
#line 31
  p = a;
  {
#line 32
  while (1) {
    while_0_continue: /* CIL Label */ ;
    {
#line 32
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 32
    if (tmp___1) {

    } else {
      goto while_0_break;
    }
#line 33
    if (flag) {
#line 34
      *((int *)p) = 1;
#line 35
      flag = 0;
    } else {
#line 37
      *((int *)p) = 2;
#line 38
      flag = 1;
    }
    {
#line 40
    __cil_tmp16 = (unsigned long )8U;
#line 40
    tmp___0 = malloc(__cil_tmp16);
#line 40
    t = (struct node *)tmp___0;
    }
    {
#line 41
    __cil_tmp17 = (List )0;
#line 41
    __cil_tmp18 = (unsigned int )__cil_tmp17;
#line 41
    __cil_tmp19 = (unsigned int )t;
#line 41
    if (__cil_tmp19 == __cil_tmp18) {
      {
#line 41
      exit(1);
      }
    } else {

    }
    }
#line 42
    __cil_tmp20 = (unsigned int )p;
#line 42
    __cil_tmp21 = __cil_tmp20 + 4;
#line 42
    *((struct node **)__cil_tmp21) = t;
#line 43
    __cil_tmp22 = (unsigned int )p;
#line 43
    __cil_tmp23 = __cil_tmp22 + 4;
#line 43
    p = *((struct node **)__cil_tmp23);
  }
  while_0_break: /* CIL Label */ ;
  }
#line 45
  *((int *)p) = 3;
  {
#line 47
  __cil_tmp24 = *((int *)a);
#line 47
  if (__cil_tmp24 == 3) {
#line 47
    return (0);
  } else {

  }
  }
#line 49
  flag = 1;
#line 50
  l1 = (struct node *)0;
#line 51
  l2 = (struct node *)0;
#line 52
  p = a;
  {
#line 53
  while (1) {
    while_1_continue: /* CIL Label */ ;
    {
#line 53
    __cil_tmp25 = *((int *)p);
#line 53
    if (__cil_tmp25 != 3) {

    } else {
      goto while_1_break;
    }
    }
#line 54
    t = p;
#line 55
    __cil_tmp26 = (unsigned int )p;
#line 55
    __cil_tmp27 = __cil_tmp26 + 4;
#line 55
    p = *((struct node **)__cil_tmp27);
#line 56
    if (flag) {
#line 57
      __cil_tmp28 = (unsigned int )t;
#line 57
      __cil_tmp29 = __cil_tmp28 + 4;
#line 57
      *((struct node **)__cil_tmp29) = l1;
#line 58
      l1 = t;
#line 59
      flag = 0;
    } else {
#line 61
      __cil_tmp30 = (unsigned int )t;
#line 61
      __cil_tmp31 = __cil_tmp30 + 4;
#line 61
      *((struct node **)__cil_tmp31) = l2;
#line 62
      l2 = t;
#line 63
      flag = 1;
    }
  }
  while_1_break: /* CIL Label */ ;
  }
#line 68
  p = l1;
  {
#line 69
  while (1) {
    while_2_continue: /* CIL Label */ ;
    {
#line 69
    __cil_tmp32 = (List )0;
#line 69
    __cil_tmp33 = (unsigned int )__cil_tmp32;
#line 69
    __cil_tmp34 = (unsigned int )p;
#line 69
    if (__cil_tmp34 != __cil_tmp33) {

    } else {
      goto while_2_break;
    }
    }
    {
#line 70
    __cil_tmp35 = *((int *)p);
#line 70
    if (__cil_tmp35 != 1) {
      goto ERROR;
    } else {

    }
    }
#line 71
    __cil_tmp36 = (unsigned int )p;
#line 71
    __cil_tmp37 = __cil_tmp36 + 4;
#line 71
    p = *((struct node **)__cil_tmp37);
  }
  while_2_break: /* CIL Label */ ;
  }
#line 73
  p = l2;
  {
#line 74
  while (1) {
    while_3_continue: /* CIL Label */ ;
    {
#line 74
    __cil_tmp38 = (List )0;
#line 74
    __cil_tmp39 = (unsigned int )__cil_tmp38;
#line 74
    __cil_tmp40 = (unsigned int )p;
#line 74
    if (__cil_tmp40 != __cil_tmp39) {

    } else {
      goto while_3_break;
    }
    }
    {
#line 75
    __cil_tmp41 = *((int *)p);
#line 75
    if (__cil_tmp41 != 2) {
      goto ERROR;
    } else {

    }
    }
#line 76
    __cil_tmp42 = (unsigned int )p;
#line 76
    __cil_tmp43 = __cil_tmp42 + 4;
#line 76
    p = *((struct node **)__cil_tmp43);
  }
  while_3_break: /* CIL Label */ ;
  }
#line 79
  return (0);
  ERROR: 
#line 81
  return (1);
}
}