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
|
[kernel] Parsing inline_def_1.i (no preprocessing)
[kernel] Parsing inline_def_2.i (no preprocessing)
/* Generated by Frama-C */
__inline static int f__fc_inline(int x)
{
return x;
}
__inline int f(int x);
__inline static int f1__fc_inline(void)
{
int __retres;
__retres = 1;
return __retres;
}
extern int f2(void)
{
int __retres;
__retres = 3;
return __retres;
}
int g(int x)
{
int __retres;
int tmp;
int tmp_0;
int tmp_1;
tmp = f__fc_inline(x);
tmp_0 = f1__fc_inline();
tmp_1 = f2();
__retres = (tmp + tmp_0) + tmp_1;
return __retres;
}
__inline int f(int x)
{
int __retres;
__retres = x + 1;
return __retres;
}
__inline static int f1__fc_inline_0(void)
{
int __retres;
__retres = 2;
return __retres;
}
int h(int x)
{
int __retres;
int tmp;
int tmp_0;
int tmp_1;
tmp = f(x);
tmp_0 = f1__fc_inline_0();
tmp_1 = f2();
__retres = (tmp + tmp_0) + tmp_1;
return __retres;
}
|
