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
|
[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_top outputs and entry point
[value] Analyzing a complete application starting at main_top
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function f <- main_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
[pdg] computing for function main_top
[pdg] warning: not implemented by pdg yet: variadic function
[pdg] Top for function 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_top
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function f <- main_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
[sparecode] select 'f' as fully visible (top or called by top)
[sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'.
/* Generated by Frama-C */
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;
}
|
