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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/sparecode/bts334.i (no preprocessing)
[value] Analyzing a complete application starting at main_init
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
kf ∈ {0}
k[0..1] ∈ {0}
e0 ∈ [--..--]
e1 ∈ [--..--]
s0 ∈ {0}
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
[value] computing for function init <- main_init.
Called from tests/sparecode/bts334.i:66.
tests/sparecode/bts334.i:66:[kernel] warning: No code nor explicit assigns clause for function init, generating default assigns from the specification
[value] using specification for function init
tests/sparecode/bts334.i:61:[value] warning: no 'assigns \result \from ...' clause specified for function init
[value] Done for function init
tests/sparecode/bts334.i:67:[value] warning: accessing uninitialized left-value. assert \initialized(&is_ok);
[value] computing for function process <- main_init.
Called from tests/sparecode/bts334.i:67.
tests/sparecode/bts334.i:53:[value] entering loop for the first time
[value] computing for function loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:53.
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:38.
tests/sparecode/bts334.i:14:[value] warning: division by zero. assert kf ≢ 0;
tests/sparecode/bts334.i:14:[value] warning: signed overflow. assert -2147483648 ≤ k[i] * (int)(vi - si[i]);
tests/sparecode/bts334.i:14:[value] warning: signed overflow. assert k[i] * (int)(vi - si[i]) ≤ 2147483647;
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:39.
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] Recording results for loop_body
[from] Computing for function loop_body
[from] Done for function loop_body
[value] Done for function loop_body
[value] computing for function loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:53.
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:38.
tests/sparecode/bts334.i:14:[value] warning: signed overflow. assert -2147483648 ≤ vi - si[i];
tests/sparecode/bts334.i:14:[value] warning: signed overflow. assert vi - si[i] ≤ 2147483647;
tests/sparecode/bts334.i:14:[value] warning: signed overflow.
assert -2147483648 ≤ (int)(so[i] / kf) + (int)(k[i] * (int)(vi - si[i]));
tests/sparecode/bts334.i:14:[value] warning: signed overflow.
assert (int)(so[i] / kf) + (int)(k[i] * (int)(vi - si[i])) ≤ 2147483647;
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:39.
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] Recording results for loop_body
[from] Computing for function loop_body
[from] Done for function loop_body
[value] Done for function loop_body
[value] computing for function loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:53.
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:38.
tests/sparecode/bts334.i:14:[value] warning: signed overflow. assert so[i] / kf ≤ 2147483647;
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] computing for function f <- loop_body <- process <- main_init.
Called from tests/sparecode/bts334.i:39.
[value] Recording results for f
[from] Computing for function f
[from] Done for function f
[value] Done for function f
[value] Recording results for loop_body
[from] Computing for function loop_body
[from] Done for function loop_body
[value] Done for function loop_body
[value] Recording results for process
[from] Computing for function process
[from] Non-terminating function process (no dependencies)
[from] Done for function process
[value] Done for function process
[value] Recording results for main_init
[from] Computing for function main_init
[from] Done for function main_init
[value] done for function main_init
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to f at tests/sparecode/bts334.i:38 (by loop_body):
si[0] FROM vi; i
so[0] FROM kf; k[0]; vi; i; si[0]; so[0]
\result FROM kf; k[0]; vi; i; si[0]; so[0]
[from] call to f at tests/sparecode/bts334.i:39 (by loop_body):
si[1] FROM vi; i
so[1] FROM kf; k[1]; vi; i; si[1]; so[1]
\result FROM kf; k[1]; vi; i; si[1]; so[1]
[from] call to loop_body at tests/sparecode/bts334.i:53 (by process):
s0 FROM kf; k[0]; e0; si[0]; so[0]
s1 FROM kf; k[1]; e1; si[1]; so[1]
si[0] FROM e0
[1] FROM e1
so[0] FROM kf; k[0]; e0; si[0]; so[0]
[1] FROM kf; k[1]; e1; si[1]; so[1]
[from] call to init at tests/sparecode/bts334.i:66 (by main_init):
is_ok FROM \nothing
\result FROM ANYTHING(origin:Unknown)
[from] call to process at tests/sparecode/bts334.i:67 (by main_init):
NON TERMINATING - NO EFFECTS
[from] entry point:
NO EFFECTS
[from] ====== END OF CALLWISE DEPENDENCIES ======
[slicing] slicing requests in progress...
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function loop_body
[pdg] done for function loop_body
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] applying all slicing requests...
[slicing] applying 1 actions...
[slicing] applying actions: 1/1...
[pdg] computing for function process
tests/sparecode/bts334.i:55:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function process
[pdg] computing for function main_init
[pdg] done for function main_init
[pdg] computing for function f
[pdg] done for function f
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
int kf;
int k[2];
int f_slice_1(int vi, int i);
static int si[2] = {0, 0};
static int so[2] = {0, 0};
int f_slice_1(int vi, int i)
{
int vo;
vo = so[i] / kf + k[i] * (vi - si[i]);
so[i] = vo;
si[i] = vi;
return vo;
}
int volatile e0;
int volatile e1;
int s0;
void loop_body_slice_1(void)
{
int acq0;
int acq1;
int val0;
/*@ slice pragma expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f_slice_1(acq0,0);
f_slice_1(acq1,1);
s0 = val0;
return;
}
void process_slice_1(int conf)
{
kf = conf;
k[0] = 3;
k[1] = 14;
while (1) loop_body_slice_1();
return;
}
extern int init(int *p);
void main_init(void)
{
int is_ok;
int config;
config = init(& is_ok);
if (is_ok) process_slice_1(config);
return;
}
|
