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 13 "list.c"
  struct node {
     int h ;
    struct node *n ;
 };
 #line 13 "list.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 9 "list.c"
  __attribute__((__nothrow__, __noreturn__)) void exit(int s ) ;
 #line 9 "list.c"
 void exit(int s ) 
 { 
 
   {
   _EXIT: 
   goto _EXIT;
 }
 }
 #line 24
 extern int ( /* missing proto */  __VERIFIER_nondet_int)() ;
 #line 18 "list.c"
 void main(void) 
 { List a ;
   void *tmp ;
   List t ;
   List p ;
   void *tmp___0 ;
   int tmp___1 ;
   void *tmp___2 ;
   int tmp___3 ;
   unsigned long __cil_tmp9 ;
   List __cil_tmp10 ;
   unsigned int __cil_tmp11 ;
   unsigned int __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   List __cil_tmp14 ;
   unsigned int __cil_tmp15 ;
   unsigned int __cil_tmp16 ;
   unsigned int __cil_tmp17 ;
   unsigned int __cil_tmp18 ;
   unsigned int __cil_tmp19 ;
   unsigned int __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   List __cil_tmp22 ;
   unsigned int __cil_tmp23 ;
   unsigned int __cil_tmp24 ;
   unsigned int __cil_tmp25 ;
   unsigned int __cil_tmp26 ;
   unsigned int __cil_tmp27 ;
   unsigned int __cil_tmp28 ;
   int __cil_tmp29 ;
   unsigned int __cil_tmp30 ;
   unsigned int __cil_tmp31 ;
   int __cil_tmp32 ;
   unsigned int __cil_tmp33 ;
   unsigned int __cil_tmp34 ;
   int __cil_tmp35 ;
 
   {
   {
 #line 20
   __cil_tmp9 = (unsigned long )8U;
 #line 20
   tmp = malloc(__cil_tmp9);
 #line 20
   a = (struct node *)tmp;
   }
   {
 #line 21
   __cil_tmp10 = (List )0;
 #line 21
   __cil_tmp11 = (unsigned int )__cil_tmp10;
 #line 21
   __cil_tmp12 = (unsigned int )a;
 #line 21
   if (__cil_tmp12 == __cil_tmp11) {
     {
 #line 21
     exit(1);
     }
   } else {
 
   }
   }
 #line 23
   p = a;
   {
 #line 24
   while (1) {
    while_0_continue: /* CIL Label */ ;
    {
#line 24
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 24
    if (tmp___1) {

    } else {
      goto while_0_break;
    }
    {
#line 25
    *((int *)p) = 1;
#line 26
    __cil_tmp13 = (unsigned long )8U;
#line 26
    tmp___0 = malloc(__cil_tmp13);
#line 26
    t = (struct node *)tmp___0;
    }
    {
#line 27
    __cil_tmp14 = (List )0;
#line 27
    __cil_tmp15 = (unsigned int )__cil_tmp14;
#line 27
    __cil_tmp16 = (unsigned int )t;
#line 27
    if (__cil_tmp16 == __cil_tmp15) {
      {
#line 27
      exit(1);
      }
    } else {

    }
    }
#line 28
    __cil_tmp17 = (unsigned int )p;
#line 28
    __cil_tmp18 = __cil_tmp17 + 4;
#line 28
    *((struct node **)__cil_tmp18) = t;
#line 29
    __cil_tmp19 = (unsigned int )p;
#line 29
    __cil_tmp20 = __cil_tmp19 + 4;
#line 29
    p = *((struct node **)__cil_tmp20);
  }
  while_0_break: /* CIL Label */ ;
  }
  {
#line 31
  while (1) {
    while_1_continue: /* CIL Label */ ;
    {
#line 31
    tmp___3 = __VERIFIER_nondet_int();
    }
#line 31
    if (tmp___3) {

    } else {
      goto while_1_break;
    }
    {
#line 32
    *((int *)p) = 2;
#line 33
    __cil_tmp21 = (unsigned long )8U;
#line 33
    tmp___2 = malloc(__cil_tmp21);
#line 33
    t = (struct node *)tmp___2;
    }
    {
#line 34
    __cil_tmp22 = (List )0;
#line 34
    __cil_tmp23 = (unsigned int )__cil_tmp22;
#line 34
    __cil_tmp24 = (unsigned int )t;
#line 34
    if (__cil_tmp24 == __cil_tmp23) {
      {
#line 34
      exit(1);
      }
    } else {

    }
    }
#line 35
    __cil_tmp25 = (unsigned int )p;
#line 35
    __cil_tmp26 = __cil_tmp25 + 4;
#line 35
    *((struct node **)__cil_tmp26) = t;
#line 36
    __cil_tmp27 = (unsigned int )p;
#line 36
    __cil_tmp28 = __cil_tmp27 + 4;
#line 36
    p = *((struct node **)__cil_tmp28);
  }
  while_1_break: /* CIL Label */ ;
  }
#line 38
  *((int *)p) = 3;
#line 41
  p = a;
  {
#line 42
  while (1) {
    while_2_continue: /* CIL Label */ ;
    {
#line 42
    __cil_tmp29 = *((int *)p);
#line 42
    if (__cil_tmp29 == 1) {

    } else {
      goto while_2_break;
    }
    }
#line 43
    __cil_tmp30 = (unsigned int )p;
#line 43
    __cil_tmp31 = __cil_tmp30 + 4;
#line 43
    p = *((struct node **)__cil_tmp31);
  }
  while_2_break: /* CIL Label */ ;
  }
  {
#line 44
  while (1) {
    while_3_continue: /* CIL Label */ ;
    {
#line 44
    __cil_tmp32 = *((int *)p);
#line 44
    if (__cil_tmp32 == 2) {

    } else {
      goto while_3_break;
    }
    }
#line 45
    __cil_tmp33 = (unsigned int )p;
#line 45
    __cil_tmp34 = __cil_tmp33 + 4;
#line 45
    p = *((struct node **)__cil_tmp34);
  }
  while_3_break: /* CIL Label */ ;
  }
  {
#line 46
  __cil_tmp35 = *((int *)p);
#line 46
  if (__cil_tmp35 != 3) {
    ERROR: 
    goto ERROR;
  } else {

  }
  }
#line 49
  return;
}
}