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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/ptr_call_object.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
[value] computing for function rand <- main.
Called from tests/value/ptr_call_object.c:30.
[value] using specification for function rand
[value] Done for function rand
[value] computing for function next_0 <- main.
Called from tests/value/ptr_call_object.c:34.
[value] Called Frama_C_show_each_p_in_next_0({{ &o0 }},
.next ∈ {{ &next_0 }}
.i ∈ UNINITIALIZED)
[value] Recording results for next_0
[value] Done for function next_0
[value] computing for function next_1 <- main.
Called from tests/value/ptr_call_object.c:34.
[value] Called Frama_C_show_each_p_in_next_1({{ &o1 }},
.next ∈ {{ &next_1 }}
.i ∈ UNINITIALIZED)
[value] Recording results for next_1
[value] Done for function next_1
[value] Called Frama_C_show_each_x({{ &o1 }})
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function next_0:
__retres ∈ {0}
[value:final-states] Values at end of function next_1:
__retres ∈ {1}
[value:final-states] Values at end of function main:
o1.next ∈ {{ &next_1 }}
.i ∈ UNINITIALIZED
o0.next ∈ {{ &next_0 }}
.i ∈ UNINITIALIZED
p ∈ {{ &o1 ; &o0 }}
__retres ∈ {0}
[from] Computing for function next_0
[from] Done for function next_0
[from] Computing for function next_1
[from] Done for function next_1
[from] Computing for function main
[from] Computing for function rand <-main
[from] Done for function rand
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function next_0:
\result FROM \nothing
[from] Function next_1:
\result FROM \nothing
[from] Function rand:
\result FROM \nothing
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function next_0:
__retres
[inout] Inputs for function next_0:
\nothing
[inout] Out (internal) for function next_1:
__retres
[inout] Inputs for function next_1:
\nothing
[inout] Out (internal) for function main:
o1.next; o0.next; p; tmp; tmp_0; __retres
[inout] Inputs for function main:
\nothing
|
