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
198
199
200
201
202
|
/* run.config*
STDOPT: +"-warn-invalid-pointer -absolute-valid-range=10-30"
STDOPT: +"-no-warn-invalid-pointer -absolute-valid-range=10-30"
*/
#include <__fc_builtin.h>
#include <stdint.h>
#include <signal.h>
/* Tests the emission of \object_pointer alarms when -warn-invalid-pointer
is enabled. The second run should emit no alarm. */
volatile int undet;
/* Simple pointer computations. */
void pointer_computation () {
int x;
int *p = &x;
if (undet)
p--; // Red alarm.
p++; // No alarm.
if (undet)
p++; // Red alarm.
int i = undet;
p += i; // Unknown alarm. [i] should be reduced to {-1, 0}.
int j = undet;
p -= j; // Unknown alarm. [j] should be reduced to {-1, 0, 1}.
p --; // Unknown alarm. [p] should be exactly {&x}.
int array[25];
int *q = undet ? &x : &array[0];
int offset1 = Frama_C_interval(0, 10);
q += offset1; // Unknown alarm. [offset1] should not be reduced.
int offset2 = Frama_C_interval(0, 50);
q += offset2; // Unknown alarm. [offset2] should be reduced to [0..25].
q += 0; // No alarm.
}
/* Increment or decrement pointers in loops. */
void pointer_in_loops () {
int t[128];
int *p = &t[0];
/*@ loop unroll 128; */
for (int i = 0; i < 128; i++) {
*p = i;
p++; // No alarm.
}
if (undet) {
int *q = &t[127];
/*@ loop unroll 128; */
for (int i = 0; i < 128; i++) {
*q = i;
q--; // Alarm in the last iteration: q points to t[-1].
}
Frama_C_show_each_bottom(q); // Should not be reached.
}
}
/* Conversion integer -> pointer. */
void int_conversion () {
int x, *p;
p = (int *)0; // NULL pointer: always ok.
p = (int *) 20; // Inside -absolute-valid-range: no alarms.
if (undet) {
p = (int *) 42; // Outside -absolute-valid-range: red alarm.
}
x = Frama_C_interval(15, 25);
p = (int *) x; // Inside -absolute-valid-range: no alarms.
x = Frama_C_interval(100, 500);
if (undet) {
p = (int *) x; // Outside -absolute-valid-range: red alarm.
}
x = Frama_C_interval(15, 100);
p = (int *) x; // Unknown alarm. [x] should be reduced to [15..31].
p = (int *) undet; // Unknown alarm. [p] should be have value in [0..31].
}
void addrof () {
int a[10], *p;
p = &(a[0]);
p = &(a[10]);
if (undet)
p = &(a[11]); // Invalid alarm
if (undet)
p = &(a[-1]); // Invalid alarm
int offset = undet;
p = &(a[offset]); /* Unknown alarm. [offset] should be reduced to [0..10]. */
}
typedef union {
uintptr_t integer;
int *pointer;
} ptr_union;
/* Creates invalid pointers through an union. */
void union_pointer () {
int *p;
ptr_union u;
u.integer = 0;
p = u.pointer; // No alarm.
if (undet) {
u.integer = 42;
p = u.pointer; // Red alarm.
}
u.integer = undet;
p = u.pointer; // Unknown alarm. [u.integer] should be reduced to [0..31].
}
/* Creates invalid pointers through untyped writes. */
void write_pointer () {
int x;
int *p = 0;
*((uintptr_t *) &p) = &x;
int *q = p; // No alarm.
*((uintptr_t *) &p) = (uintptr_t)p + undet;
q = p; // Unknown alarm.
*((uintptr_t *) &p) = 42;
if (undet) {
q = p; // Red alarm.
}
}
/* Tests the evaluation of the logical predicate \object_pointer when
-warn-invalid-pointer is disabled. */
void object_pointer_predicate () {
int x, array[64];
int *p = &x;
/*@ assert \object_pointer(p); */
if (undet) {
p--;
/*@ assert \object_pointer(p); */
}
p++;
/*@ assert \object_pointer(p); */
if (undet) {
p++;
/*@ assert \object_pointer(p); */
}
p += undet;
/*@ assert \object_pointer(p); */
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer(p);
p = (int *)((uintptr_t)&x + undet);
/*@ assert \object_pointer(p); */
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer_char(p);
int i = Frama_C_interval(0, 20);
p = undet ? &x : &array[i];
/*@ assert \object_pointer(p); */
p += i;
/*@ assert \object_pointer(p); */
p += undet;
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer_array(p);
p = (int *) 0;
/*@ assert \object_pointer(p); */
if (undet)
p = (int *) 20;
/*@ assert \object_pointer(p); */
if (undet)
p = (int *) 50;
/*@ assert \object_pointer(p); */
p = (int *) undet;
/*@ assert \object_pointer(p); */
if (undet) {
p = (int *) 100;
/*@ assert \object_pointer(p); */
}
}
/* CERT C UB 62. An attempt is made to access, or generate a pointer to just
past, a flexible array member of a structure when the referenced object
provides no elements for that array (6.7.2.1). */
struct sfam {
int len;
char fam[];
};
void flexible_array_member() {
struct sfam s1 = { 0 };
if (undet) {
char *p = s1.fam + 1; // UB 62 (generate a pointer ...)
}
if (undet) {
char *p = s1.fam;
*(p+1) = 0; // UB 62 (access a pointer ...)
}
}
void main () {
pointer_computation ();
pointer_in_loops ();
int_conversion ();
addrof ();
union_pointer ();
write_pointer ();
object_pointer_predicate ();
flexible_array_member();
// should not emit an alarm
signal (SIGUSR1, SIG_IGN);
signal (SIGUSR2, SIG_ERR);
signal (SIGUNUSED, SIG_DFL);
}
|
