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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/sparecode/top.i (no preprocessing)
[sparecode] remove unused code...
[sparecode] selecting function main_call_top outputs and entry point
[value] Analyzing a complete application starting at main_call_top
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function main_top <- main_call_top.
Called from tests/sparecode/top.i:26.
[value] computing for function f <- main_top <- main_call_top.
Called from tests/sparecode/top.i:21.
[value] Recording results for f
[value] Done for function f
[value] Recording results for main_top
[value] Done for function main_top
[value] computing for function not_used_in_main_top <- main_call_top.
Called from tests/sparecode/top.i:27.
[value] computing for function print <- not_used_in_main_top <- main_call_top.
Called from tests/sparecode/top.i:10.
tests/sparecode/top.i:10:[kernel] warning: Neither code nor specification for function print, generating default assigns from the prototype
[value] using specification for function print
[value] Done for function print
[value] Recording results for not_used_in_main_top
[value] Done for function not_used_in_main_top
[value] Recording results for main_call_top
[value] done for function main_call_top
[pdg] computing for function main_call_top
[from] Computing for function main_top
[from] Computing for function f <-main_top
[from] Done for function f
[from] Done for function main_top
[from] Computing for function not_used_in_main_top
[from] Computing for function print <-not_used_in_main_top
[from] Done for function print
[from] Done for function not_used_in_main_top
[pdg] done for function main_call_top
[sparecode] add selection in function 'main_call_top'
[sparecode] selecting output zones \nothing
[sparecode] add selection in function 'main_call_top'
[pdg] computing for function not_used_in_main_top
[pdg] done for function not_used_in_main_top
[pdg] computing for function main_top
[pdg] warning: not implemented by pdg yet: variadic function
[pdg] Top for function main_top
[sparecode] memo call to TOP 'main_top'
[sparecode] select 'main_top' as fully visible (top or called by top)
[users] requiring again the computation of the value analysis
[value] Analyzing a complete application starting at main_call_top
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function main_top <- main_call_top.
Called from tests/sparecode/top.i:26.
[value] computing for function f <- main_top <- main_call_top.
Called from tests/sparecode/top.i:21.
[value] Recording results for f
[value] Done for function f
[value] Recording results for main_top
[value] Done for function main_top
[value] computing for function not_used_in_main_top <- main_call_top.
Called from tests/sparecode/top.i:27.
[value] computing for function print <- not_used_in_main_top <- main_call_top.
Called from tests/sparecode/top.i:10.
[value] Done for function print
[value] Recording results for not_used_in_main_top
[value] Done for function not_used_in_main_top
[value] Recording results for main_call_top
[value] done for function main_call_top
[sparecode] select 'f' as fully visible (top or called by top)
[sparecode] look for annotations in function Frama_C_bzero
[pdg] computing for function Frama_C_bzero
[from] Computing for function Frama_C_bzero
[from] Done for function Frama_C_bzero
[pdg] done for function Frama_C_bzero
[sparecode] look for annotations in function Frama_C_copy_block
[pdg] computing for function Frama_C_copy_block
[from] Computing for function Frama_C_copy_block
[from] Done for function Frama_C_copy_block
[pdg] done for function Frama_C_copy_block
[sparecode] look for annotations in function f
[pdg] computing for function f
[pdg] done for function f
[sparecode] look for annotations in function main_call_top
[pdg] computing for function main_call_top
[from] Computing for function main_top
[from] Computing for function f <-main_top
[from] Done for function f
[from] Done for function main_top
[from] Computing for function not_used_in_main_top
[from] Computing for function print <-not_used_in_main_top
[from] Done for function print
[from] Done for function not_used_in_main_top
[pdg] done for function main_call_top
[sparecode] look for annotations in function main_top
[pdg] computing for function main_top
[pdg] warning: not implemented by pdg yet: variadic function
[pdg] Top for function main_top
[sparecode] pdg top: skip annotations
[sparecode] look for annotations in function main_top_not_used
[pdg] computing for function main_top_not_used
[pdg] warning: unreachable entry point (sid:18, function main_top_not_used)
[pdg] Bottom for function main_top_not_used
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function not_used_in_main_top
[pdg] computing for function not_used_in_main_top
[pdg] done for function not_used_in_main_top
[sparecode] look for annotations in function print
[pdg] computing for function print
[pdg] done for function print
[sparecode] finalize call input propagation
[sparecode] add selection in function 'main_call_top'
[sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'.
/* Generated by Frama-C */
int not_used_in_main_top(int x)
{
int __retres;
__retres = x + 2;
return __retres;
}
int f(int a)
{
int __retres;
__retres = a + 1;
return __retres;
}
int main_top(int nb , ...)
{
int x;
int y;
x = 3;
y = f(2);
return x;
}
int main_call_top(void)
{
int x;
x = main_top(2,0,1);
x = not_used_in_main_top(x);
return x;
}
|
