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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/sparecode/bts334.i (no preprocessing)
[slicing] slicing requests in progress...
[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
[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
[value] Done for function f
[value] Recording results for 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
[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
[value] Done for function f
[value] Recording results for 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
[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
[value] Done for function f
[value] Recording results for loop_body
[value] Done for function loop_body
[value] Recording results for process
[value] Done for function process
[value] Recording results for main_init
[value] done for function main_init
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function loop_body
[from] Computing for function f
[from] Done for function f
[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
[from] Computing for function loop_body
[from] Done for function loop_body
tests/sparecode/bts334.i:55:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function process
[pdg] computing for function main_init
[from] Computing for function init
[from] Done for function init
[from] Computing for function process
[from] Non-terminating function process (no dependencies)
[from] Done for function process
[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;
}
|
