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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/attribute-aligned.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
S ∈ {0}
A ∈ {0}
B ∈ {0}
[value] computing for function ct <- main.
Called from tests/value/attribute-aligned.c:94.
[value] Recording results for ct
[value] Done for function ct
[value] computing for function dt <- main.
Called from tests/value/attribute-aligned.c:95.
[value] Recording results for dt
[value] Done for function dt
[value] computing for function pt <- main.
Called from tests/value/attribute-aligned.c:96.
[value] Recording results for pt
[value] Done for function pt
[value] computing for function qt <- main.
Called from tests/value/attribute-aligned.c:97.
[value] Recording results for qt
[value] Done for function qt
[value] computing for function rt <- main.
Called from tests/value/attribute-aligned.c:98.
[value] Recording results for rt
[value] Done for function rt
[value] computing for function st <- main.
Called from tests/value/attribute-aligned.c:99.
[value] Recording results for st
[value] Done for function st
[value] computing for function tt <- main.
Called from tests/value/attribute-aligned.c:100.
[value] Recording results for tt
[value] Done for function tt
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function ct:
S ∈ {1}
A ∈ {0}
[value:final-states] Values at end of function dt:
S ∈ {4}
A ∈ {0}
[value:final-states] Values at end of function pt:
S ∈ {4}
A ∈ {0}
[value:final-states] Values at end of function qt:
S ∈ {4}
A ∈ {0}
B ∈ {1}
[value:final-states] Values at end of function rt:
S ∈ {8}
A ∈ {0}
B ∈ {4}
[value:final-states] Values at end of function st:
S ∈ {8}
A ∈ {0}
B ∈ {4}
[value:final-states] Values at end of function tt:
S ∈ {4}
A ∈ {0}
B ∈ {4}
[value:final-states] Values at end of function main:
S ∈ {4}
A ∈ {0}
B ∈ {4}
__retres ∈ {0}
[from] Computing for function ct
[from] Done for function ct
[from] Computing for function dt
[from] Done for function dt
[from] Computing for function pt
[from] Done for function pt
[from] Computing for function qt
[from] Done for function qt
[from] Computing for function rt
[from] Done for function rt
[from] Computing for function st
[from] Done for function st
[from] Computing for function tt
[from] Done for function tt
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function ct:
S FROM \nothing
A FROM \nothing
[from] Function dt:
S FROM \nothing
A FROM \nothing
[from] Function pt:
S FROM \nothing
A FROM \nothing
[from] Function qt:
S FROM \nothing
A FROM \nothing
B FROM \nothing
[from] Function rt:
S FROM \nothing
A FROM \nothing
B FROM \nothing
[from] Function st:
S FROM \nothing
A FROM \nothing
B FROM \nothing
[from] Function tt:
S FROM \nothing
A FROM \nothing
B FROM \nothing
[from] Function main:
S FROM \nothing
A FROM \nothing
B FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function ct:
S; A
[inout] Inputs for function ct:
\nothing
[inout] Out (internal) for function dt:
S; A
[inout] Inputs for function dt:
\nothing
[inout] Out (internal) for function pt:
S; A
[inout] Inputs for function pt:
\nothing
[inout] Out (internal) for function qt:
S; A; B
[inout] Inputs for function qt:
\nothing
[inout] Out (internal) for function rt:
S; A; B
[inout] Inputs for function rt:
\nothing
[inout] Out (internal) for function st:
S; A; B
[inout] Inputs for function st:
\nothing
[inout] Out (internal) for function tt:
S; A; B
[inout] Inputs for function tt:
\nothing
[inout] Out (internal) for function main:
S; A; B; __retres
[inout] Inputs for function main:
\nothing
|
