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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/sparecode/bts334.i (no preprocessing)
[sparecode] remove unused code...
[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
[pdg] computing for function main_init
[from] Computing for function init
[from] Done for function init
[from] Computing for function process
[from] Computing for function loop_body <-process
[from] Computing for function f <-loop_body <-process
[from] Done for function f
[from] Done for function loop_body
[from] Non-terminating function process (no dependencies)
[from] Done for function process
[pdg] done for function main_init
[pdg] computing for function Frama_C_bzero
[from] Computing for function Frama_C_bzero
[from] Done for function Frama_C_bzero
[pdg] done for function Frama_C_bzero
[pdg] computing for function Frama_C_copy_block
[from] Computing for function Frama_C_copy_block
[from] Done for function Frama_C_copy_block
[pdg] done for function Frama_C_copy_block
[pdg] computing for function f
[pdg] done for function f
[pdg] computing for function init
[pdg] done for function init
[pdg] computing for function loop_body
[pdg] done for function loop_body
[pdg] computing for function process
tests/sparecode/bts334.i:55:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function process
[sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'.
/* Generated by Frama-C */
int kf;
int k[2];
int f(int vi, int i);
static int si[2] = {0, 0};
static int so[2] = {0, 0};
int f(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(void)
{
int acq0;
int acq1;
int val0;
/*@ slice pragma expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f(acq0,0);
f(acq1,1);
s0 = val0;
return;
}
void process(int conf)
{
kf = conf;
k[0] = 3;
k[1] = 14;
while (1) loop_body();
return;
}
/*@ assigns *p;
assigns *p \from \nothing;
behavior default:
assigns *p;
assigns *p \from \nothing;
*/
extern int init(int *p);
void main_init(void)
{
int is_ok;
int config;
config = init(& is_ok);
if (is_ok) process(config);
return;
}
|
