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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/redundant_alarms.c (with preprocessing)
[slicing] slicing requests in progress...
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
v ∈ [--..--]
[value] computing for function main1 <- main.
Called from tests/value/redundant_alarms.c:50.
tests/value/redundant_alarms.c:11:[value] warning: accessing uninitialized left-value. assert \initialized(p);
tests/value/redundant_alarms.c:12:[value] warning: accessing uninitialized left-value. assert \initialized(p);
tests/value/redundant_alarms.c:15:[value] warning: accessing uninitialized left-value. assert \initialized(p);
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
Called from tests/value/redundant_alarms.c:51.
tests/value/redundant_alarms.c:20:[value] warning: accessing out of bounds index. assert 0 ≤ i;
tests/value/redundant_alarms.c:20:[value] warning: accessing out of bounds index. assert i < 10;
tests/value/redundant_alarms.c:21:[value] warning: accessing uninitialized left-value. assert \initialized(&t[i]);
tests/value/redundant_alarms.c:22:[value] warning: accessing uninitialized left-value. assert \initialized(&t[i]);
[value] Recording results for main2
[value] Done for function main2
[value] computing for function main3 <- main.
Called from tests/value/redundant_alarms.c:52.
tests/value/redundant_alarms.c:25:[value] warning: function main3: precondition got status unknown.
tests/value/redundant_alarms.c:31:[value] warning: accessing uninitialized left-value. assert \initialized(&t[i]);
tests/value/redundant_alarms.c:31:[value] warning: accessing uninitialized left-value. assert \initialized(&t[j]);
tests/value/redundant_alarms.c:32:[value] warning: accessing uninitialized left-value. assert \initialized(&t[j]);
tests/value/redundant_alarms.c:33:[value] warning: accessing uninitialized left-value. assert \initialized(&t[i]);
[value] Recording results for main3
[value] Done for function main3
[value] computing for function main4 <- main.
Called from tests/value/redundant_alarms.c:53.
tests/value/redundant_alarms.c:39:[value] entering loop for the first time
tests/value/redundant_alarms.c:41:[value] warning: assertion got status unknown.
[value] Recording results for main4
[value] Done for function main4
[value] Recording results for main
[value] done for function main
tests/value/redundant_alarms.c:15:[value] assertion 'Value,initialisation' got final status invalid.
[scope:rm_asserts] removing 3 assertion(s)
tests/value/redundant_alarms.c:12:[scope:rm_asserts] removing redundant assert Value: initialisation: \initialized(p);
tests/value/redundant_alarms.c:32:[scope:rm_asserts] removing redundant assert Value: initialisation: \initialized(&t[j]);
tests/value/redundant_alarms.c:33:[scope:rm_asserts] removing redundant assert Value: initialisation: \initialized(&t[i]);
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function main1
[pdg] done for function main1
[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 main
[from] Computing for function main1
[from] Done for function main1
[from] Computing for function main2
[from] Done for function main2
[from] Computing for function main3
[from] Done for function main3
[from] Computing for function main4
[from] Non-terminating function main4 (no dependencies)
[from] Done for function main4
[pdg] done for function main
[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 volatile v;
void main1(int c)
{
int x;
int y;
int t;
int *p;
int *tmp;
int z;
int w;
if (c) tmp = & x; else tmp = & y;
p = tmp;
*p = 1;
/*@ assert Value: initialisation: \initialized(p); */
z = *p + 1;
/*@ assert Value: initialisation: \initialized(p); */
w = *p + 2;
x = t;
y = t;
x = t;
if (v)
/*@ assert Value: initialisation: \initialized(p); */
z = *p + 2;
return;
}
void main2(int i)
{
int t[10];
/*@ assert Value: index_bound: 0 ≤ i; */
/*@ assert Value: index_bound: i < 10; */
t[i] = 1;
/*@ assert Value: initialisation: \initialized(&t[i]); */
t[i] += 3;
/*@ assert Value: initialisation: \initialized(&t[i]); */
t[i] += 5;
return;
}
/*@ requires i < 10 ∧ j < 10; */
void main3(unsigned int i, unsigned int j)
{
int t[10];
if (v) t[i] = v;
/*@ assert Value: initialisation: \initialized(&t[i]); */
/*@ assert Value: initialisation: \initialized(&t[j]); */
if (t[i] < t[j]) {
int tmp;
/*@ assert Value: initialisation: \initialized(&t[j]); */
tmp = t[j];
/*@ assert Value: initialisation: \initialized(&t[i]); */
t[j] = t[i];
t[i] = tmp;
}
return;
}
void main4(int i)
{
while (1) {
{
int j;
int k;
int z;
int w;
j = 0;
/*@ assert i ≤ 0; */ ;
k = 0;
z = 0;
w = 0;
}
}
return;
}
void main(void)
{
if (v) main1(v);
main2(v);
main3((unsigned int)v,(unsigned int)v);
if (v) main4(v);
return;
}
/* Generated by Frama-C */
int volatile v;
void main1_slice_1(int c)
{
int x;
int y;
int t;
int *p;
int *tmp;
int z;
int w;
if (c) tmp = & x; else tmp = & y;
p = tmp;
*p = 1;
z = *p + 1;
w = *p + 2;
y = t;
x = t;
if (v) z = *p + 2;
return;
}
void main(void)
{
if (v) main1_slice_1(v);
return;
}
|
