File: enum_repr.1.res.oracle

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 42,324 kB
  • ctags: 35,695
  • sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (165 lines) | stat: -rw-r--r-- 4,515 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/enum_repr.i (no preprocessing)
tests/syntax/enum_repr.i:37:[kernel] Inserted implicit cast from int to enum __anonenum_foo_1
tests/syntax/enum_repr.i:38:[kernel] Inserted implicit cast from int to enum __anonenum_bar_2
tests/syntax/enum_repr.i:39:[kernel] Inserted implicit cast from int to enum __anonenum_bu1_3
tests/syntax/enum_repr.i:41:[kernel] Inserted implicit cast from long long to enum __anonenum_bu3_5
tests/syntax/enum_repr.i:43:[kernel] Inserted implicit cast from unsigned int to enum __anonenum_bs2_7
tests/syntax/enum_repr.i:45:[kernel] Inserted implicit cast from signed char to enum __anonenum_bc1_9
tests/syntax/enum_repr.i:48:[kernel] Inserted implicit cast from unsigned char to enum __anonenum_bd2_12
tests/syntax/enum_repr.i:49:[kernel] Inserted implicit cast from foo to int
tests/syntax/enum_repr.i:49:[kernel] Inserted implicit cast from bar to int
tests/syntax/enum_repr.i:63:[kernel] Inserted implicit cast from int to enum __anonenum_foo_1
tests/syntax/enum_repr.i:66:[kernel] Inserted implicit cast from enum __anonenum_foo_1 to unsigned int
tests/syntax/enum_repr.i:67:[kernel] Inserted implicit cast from unsigned int to enum __anonenum_foo_1
tests/syntax/enum_repr.i:68:[kernel] Inserted implicit cast from unsigned int to enum __anonenum_foo_1
[kernel] Enum __anonenum_foo_1 is represented by unsigned char
[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 char
[kernel] Enum __anonenum_bc2_10 is represented by unsigned char
[kernel] Enum __anonenum_bd1_11 is represented by signed char
[kernel] Enum __anonenum_bd2_12 is represented by signed char
/* 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;
  bar y;
  bu1 u1;
  bu2 u2;
  bu3 u3;
  bs1 s1;
  bs2 s2;
  bs3 s3;
  bc1 c1;
  bc2 c2;
  bd1 d1;
  bd2 d2;
  x = (enum __anonenum_foo_1)A;
  y = (enum __anonenum_bar_2)B;
  u1 = Bu1;
  u2 = Bu2;
  u3 = Bu3;
  s1 = Bs1;
  s2 = (enum __anonenum_bs2_7)Bs2;
  s3 = Bs3;
  c1 = Bc1;
  c2 = Bc2;
  d1 = Bd1;
  d2 = Bd2;
  if ((int)x == A) 
    if ((int)y == B) {
      __retres = 0;
      goto return_label;
    }
  __retres = 1;
  return_label: return __retres;
}

extern int f1(bla x);

extern int f2(bla x);

extern int f3(bla x);

extern int h1(foo x);

extern int h2(foo x);

extern int h3(foo x);

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