enum_repr.2.res.oracle

[kernel] Parsing tests/syntax/enum_repr.i (no preprocessing)
[kernel] tests/syntax/enum_repr.i:37: 
  Inserted implicit cast from int to enum __anonenum_foo_1
[kernel] tests/syntax/enum_repr.i:38: 
  Inserted implicit cast from int to enum __anonenum_bar_2
[kernel] tests/syntax/enum_repr.i:39: 
  Inserted implicit cast from int to enum __anonenum_bu1_3
[kernel] tests/syntax/enum_repr.i:41: 
  Inserted implicit cast from long long to enum __anonenum_bu3_5
[kernel] tests/syntax/enum_repr.i:43: 
  Inserted implicit cast from unsigned int to enum __anonenum_bs2_7
[kernel] tests/syntax/enum_repr.i:45: 
  Inserted implicit cast from signed char to enum __anonenum_bc1_9
[kernel] tests/syntax/enum_repr.i:46: 
  Inserted implicit cast from unsigned char to enum __anonenum_bc2_10
[kernel] tests/syntax/enum_repr.i:47: 
  Inserted implicit cast from signed char to enum __anonenum_bd1_11
[kernel] tests/syntax/enum_repr.i:48: 
  Inserted implicit cast from unsigned char to enum __anonenum_bd2_12
[kernel] tests/syntax/enum_repr.i:49: 
  Inserted implicit cast from int to unsigned int
[kernel] tests/syntax/enum_repr.i:49: Inserted implicit cast from bar to int
[kernel] tests/syntax/enum_repr.i:63: 
  Inserted implicit cast from int to enum __anonenum_foo_1
[kernel] Enum __anonenum_foo_1 is represented by unsigned int
[kernel] Enum __anonenum_bar_2 is represented by unsigned char
[kernel] Enum __anonenum_bu1_3 is represented by unsigned int
[kernel] Enum __anonenum_bu2_4 is represented by unsigned int
[kernel] Enum __anonenum_bu3_5 is represented by unsigned long long
[kernel] Enum __anonenum_bs1_6 is represented by int
[kernel] Enum __anonenum_bs2_7 is represented by long long
[kernel] Enum __anonenum_bs3_8 is represented by long long
[kernel] Enum __anonenum_bc1_9 is represented by unsigned int
[kernel] Enum __anonenum_bc2_10 is represented by unsigned int
[kernel] Enum __anonenum_bd1_11 is represented by int
[kernel] Enum __anonenum_bd2_12 is represented by int
/* Generated by Frama-C */
enum __anonenum_foo_1 {
    A = 3
};
typedef enum __anonenum_foo_1 foo;
enum __anonenum_bar_2 {
    B = 6
} __attribute__((__packed__));
typedef enum __anonenum_bar_2 bar;
enum __anonenum_bu1_3 {
    Bu1 = 0x7FFFFFFF
};
typedef enum __anonenum_bu1_3 bu1;
enum __anonenum_bu2_4 {
    Bu2 = 0xFFFFFFFF
};
typedef enum __anonenum_bu2_4 bu2;
enum __anonenum_bu3_5 {
    Bu3 = 0x1FFFFFFFF
};
typedef enum __anonenum_bu3_5 bu3;
enum __anonenum_bs1_6 {
    Bs1 = 0x7FFFFFFF,
    Ms1 = -1
};
typedef enum __anonenum_bs1_6 bs1;
enum __anonenum_bs2_7 {
    Bs2 = 0xFFFFFFFF,
    Ms2 = -1
};
typedef enum __anonenum_bs2_7 bs2;
enum __anonenum_bs3_8 {
    Bs3 = 0x1FFFFFFFF,
    Ms3 = -1
};
typedef enum __anonenum_bs3_8 bs3;
enum __anonenum_bc1_9 {
    Bc1 = (signed char)'c'
};
typedef enum __anonenum_bc1_9 bc1;
enum __anonenum_bc2_10 {
    Bc2 = (unsigned char)'c'
};
typedef enum __anonenum_bc2_10 bc2;
enum __anonenum_bd1_11 {
    Bd1 = (signed char)'c',
    Md1 = -1
};
typedef enum __anonenum_bd1_11 bd1;
enum __anonenum_bd2_12 {
    Bd2 = (unsigned char)'c',
    Md2 = -1
};
typedef enum __anonenum_bd2_12 bd2;
typedef unsigned int bla;
int main(void)
{
  int __retres;
  foo x = A;
  bar y = (enum __anonenum_bar_2)B;
  bu1 u1 = Bu1;
  bu2 u2 = Bu2;
  bu3 u3 = Bu3;
  bs1 s1 = Bs1;
  bs2 s2 = (enum __anonenum_bs2_7)Bs2;
  bs3 s3 = Bs3;
  bc1 c1 = (enum __anonenum_bc1_9)Bc1;
  bc2 c2 = (enum __anonenum_bc2_10)Bc2;
  bd1 d1 = (enum __anonenum_bd1_11)Bd1;
  bd2 d2 = (enum __anonenum_bd2_12)Bd2;
  if (x == (unsigned int)A) 
    if ((int)y == B) {
      __retres = 0;
      goto return_label;
    }
  __retres = 1;
  return_label: return __retres;
}

int f1(bla x);

int f2(bla x);

int f3(bla x);

int h1(foo x);

int h2(foo x);

int h3(foo x);

int g(void)
{
  int tmp_0;
  int tmp_1;
  int tmp_2;
  int tmp_3;
  int tmp_4;
  foo x = A;
  int res = f1((unsigned int)x);
  tmp_0 = f2((unsigned int)x);
  res += tmp_0;
  tmp_1 = f3(x);
  res += tmp_1;
  tmp_2 = h1((unsigned int)x);
  res += tmp_2;
  tmp_3 = h2((unsigned int)x);
  res += tmp_3;
  tmp_4 = h3(x);
  res += tmp_4;
  return res;
}