[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/gcc_builtins.c (with preprocessing)
/* Generated by Frama-C */
typedef short int16_t;
typedef unsigned short uint16_t;
typedef int int32_t;
typedef unsigned int uint32_t;
typedef long long int64_t;
typedef unsigned long long uint64_t;
/* compiler builtin: 
   short __sync_add_and_fetch_int16_t(short *ptr, short value , ...);   */
/* compiler builtin: 
   int __sync_add_and_fetch_int32_t(int *ptr, int value , ...);   */
/* compiler builtin: 
   long long __sync_add_and_fetch_int64_t(long long *ptr, long long value
                                          , ...);   */
/* compiler builtin: 
   int __sync_bool_compare_and_swap_uint16_t(unsigned short *ptr,
                                             unsigned short oldval,
                                             unsigned short newval , ...);   */
/* compiler builtin: 
   int __sync_bool_compare_and_swap_uint32_t(unsigned int *ptr,
                                             unsigned int oldval,
                                             unsigned int newval , ...);   */
/* compiler builtin: 
   int __sync_bool_compare_and_swap_uint64_t(unsigned long long *ptr,
                                             unsigned long long oldval,
                                             unsigned long long newval , ...);   */
/* compiler builtin: 
   short __sync_fetch_and_add_int16_t(short *ptr, short value , ...);   */
/* compiler builtin: 
   int __sync_fetch_and_add_int32_t(int *ptr, int value , ...);   */
/* compiler builtin: 
   long long __sync_fetch_and_add_int64_t(long long *ptr, long long value
                                          , ...);   */
/* compiler builtin: 
   short __sync_fetch_and_sub_int16_t(short *ptr, short value , ...);   */
/* compiler builtin: 
   int __sync_fetch_and_sub_int32_t(int *ptr, int value , ...);   */
/* compiler builtin: 
   long long __sync_fetch_and_sub_int64_t(long long *ptr, long long value
                                          , ...);   */
/* compiler builtin: 
   short __sync_sub_and_fetch_int16_t(short *ptr, short value , ...);   */
/* compiler builtin: 
   int __sync_sub_and_fetch_int32_t(int *ptr, int value , ...);   */
/* compiler builtin: 
   long long __sync_sub_and_fetch_int64_t(long long *ptr, long long value
                                          , ...);   */
short __sync_fetch_and_add_int16_t(short *ptr, short value , ...)
{
  int16_t tmp;
  tmp = *ptr;
  *ptr = (short)((int)*ptr + (int)value);
  return tmp;
}

short __sync_fetch_and_sub_int16_t(short *ptr, short value , ...)
{
  int16_t tmp;
  tmp = *ptr;
  *ptr = (short)((int)*ptr - (int)value);
  return tmp;
}

int __sync_fetch_and_add_int32_t(int *ptr, int value , ...)
{
  int32_t tmp;
  tmp = *ptr;
  *ptr += value;
  return tmp;
}

int __sync_fetch_and_sub_int32_t(int *ptr, int value , ...)
{
  int32_t tmp;
  tmp = *ptr;
  *ptr -= value;
  return tmp;
}

long long __sync_fetch_and_add_int64_t(long long *ptr, long long value , ...)
{
  int64_t tmp;
  tmp = *ptr;
  *ptr += value;
  return tmp;
}

long long __sync_fetch_and_sub_int64_t(long long *ptr, long long value , ...)
{
  int64_t tmp;
  tmp = *ptr;
  *ptr -= value;
  return tmp;
}

short __sync_add_and_fetch_int16_t(short *ptr, short value , ...)
{
  short __retres;
  *ptr = (short)((int)*ptr + (int)value);
  __retres = *ptr;
  return __retres;
}

short __sync_sub_and_fetch_int16_t(short *ptr, short value , ...)
{
  short __retres;
  *ptr = (short)((int)*ptr - (int)value);
  __retres = *ptr;
  return __retres;
}

int __sync_add_and_fetch_int32_t(int *ptr, int value , ...)
{
  int __retres;
  *ptr += value;
  __retres = *ptr;
  return __retres;
}

int __sync_sub_and_fetch_int32_t(int *ptr, int value , ...)
{
  int __retres;
  *ptr -= value;
  __retres = *ptr;
  return __retres;
}

long long __sync_add_and_fetch_int64_t(long long *ptr, long long value , ...)
{
  long long __retres;
  *ptr += value;
  __retres = *ptr;
  return __retres;
}

long long __sync_sub_and_fetch_int64_t(long long *ptr, long long value , ...)
{
  long long __retres;
  *ptr -= value;
  __retres = *ptr;
  return __retres;
}

int __sync_bool_compare_and_swap_uint16_t(unsigned short *ptr,
                                          unsigned short oldval,
                                          unsigned short newval , ...)
{
  int __retres;
  if ((int)*ptr == (int)oldval) {
    *ptr = newval;
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

int __sync_bool_compare_and_swap_uint32_t(unsigned int *ptr,
                                          unsigned int oldval,
                                          unsigned int newval , ...)
{
  int __retres;
  if (*ptr == oldval) {
    *ptr = newval;
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

int __sync_bool_compare_and_swap_uint64_t(unsigned long long *ptr,
                                          unsigned long long oldval,
                                          unsigned long long newval , ...)
{
  int __retres;
  if (*ptr == oldval) {
    *ptr = newval;
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

void main(void)
{
  int x_1;
  int tmp;
  {
    int16_t content;
    int16_t *ptr;
    int16_t value;
    int16_t result;
    content = (short)100;
    ptr = & content;
    value = (short)33;
    result = __sync_fetch_and_add_int16_t(ptr,value);
    /*@ assert result ≡ 100 ∧ content ≡ 133; */ ;
    result = __sync_fetch_and_add_int16_t(ptr,(short)(-11));
    /*@ assert result ≡ 133 ∧ content ≡ 122; */ ;
    result = __sync_fetch_and_sub_int16_t(ptr,value);
    /*@ assert result ≡ 122 ∧ content ≡ 89; */ ;
    result = __sync_fetch_and_sub_int16_t(ptr,(short)(-11));
    /*@ assert result ≡ 89 ∧ content ≡ 100; */ ;
  }
  {
    int32_t content_0;
    int32_t *ptr_0;
    int32_t value_0;
    int32_t result_0;
    content_0 = 100;
    ptr_0 = & content_0;
    value_0 = 33;
    result_0 = __sync_fetch_and_add_int32_t(ptr_0,value_0);
    /*@ assert result_0 ≡ 100 ∧ content_0 ≡ 133; */ ;
    result_0 = __sync_fetch_and_add_int32_t(ptr_0,-11);
    /*@ assert result_0 ≡ 133 ∧ content_0 ≡ 122; */ ;
    result_0 = __sync_fetch_and_sub_int32_t(ptr_0,value_0);
    /*@ assert result_0 ≡ 122 ∧ content_0 ≡ 89; */ ;
    result_0 = __sync_fetch_and_sub_int32_t(ptr_0,-11);
    /*@ assert result_0 ≡ 89 ∧ content_0 ≡ 100; */ ;
  }
  {
    int64_t content_1;
    int64_t *ptr_1;
    int64_t value_1;
    int64_t result_1;
    content_1 = (long long)100;
    ptr_1 = & content_1;
    value_1 = (long long)33;
    result_1 = __sync_fetch_and_add_int64_t(ptr_1,value_1);
    /*@ assert result_1 ≡ 100 ∧ content_1 ≡ 133; */ ;
    result_1 = __sync_fetch_and_add_int64_t(ptr_1,(long long)(-11));
    /*@ assert result_1 ≡ 133 ∧ content_1 ≡ 122; */ ;
    result_1 = __sync_fetch_and_sub_int64_t(ptr_1,value_1);
    /*@ assert result_1 ≡ 122 ∧ content_1 ≡ 89; */ ;
    result_1 = __sync_fetch_and_sub_int64_t(ptr_1,(long long)(-11));
    /*@ assert result_1 ≡ 89 ∧ content_1 ≡ 100; */ ;
  }
  {
    uint16_t content_2;
    uint16_t *ptr_2;
    uint16_t oldval;
    uint16_t newval;
    int result_2;
    content_2 = (unsigned short)100;
    ptr_2 = & content_2;
    oldval = (unsigned short)100;
    newval = (unsigned short)133;
    result_2 = __sync_bool_compare_and_swap_uint16_t(ptr_2,oldval,newval);
    /*@ assert result_2 ≡ 1 ∧ *ptr_2 ≡ newval; */ ;
  }
  {
    uint32_t content_3;
    uint32_t *ptr_3;
    uint32_t oldval_0;
    uint32_t newval_0;
    int result_3;
    content_3 = (unsigned int)100;
    ptr_3 = & content_3;
    oldval_0 = (unsigned int)100;
    newval_0 = (unsigned int)133;
    result_3 = __sync_bool_compare_and_swap_uint32_t(ptr_3,oldval_0,newval_0);
    /*@ assert result_3 ≡ 1 ∧ *ptr_3 ≡ newval_0; */ ;
  }
  {
    uint64_t content_4;
    uint64_t *ptr_4;
    uint64_t oldval_1;
    uint64_t newval_1;
    int result_4;
    content_4 = (unsigned long long)100;
    ptr_4 = & content_4;
    oldval_1 = (unsigned long long)100;
    newval_1 = (unsigned long long)133;
    result_4 = __sync_bool_compare_and_swap_uint64_t(ptr_4,oldval_1,newval_1);
    /*@ assert result_4 ≡ 1 ∧ *ptr_4 ≡ newval_1; */ ;
  }
  if ((long)(4 == 4)) {
    int x;
    x = 1;
  }
  if ((long)(3 == 4)) {
    int x_0;
    x_0 = 0;
  }
  x_1 = 2;
  { /* sequence */
    ;
    tmp = x_1;
    x_1 ++;
    ;
  }
  if ((long)tmp) {
    int y;
    y = x_1;
  }
  return;
}