Язык C позволяет использовать операторы, которые приводят переменную в качестве пустого указателя. Однако Polyspace® верификация этих операторов влечет за собой потерю точности.
Примите во внимание:
1 typedef struct {
2 int x1;
3 } s1;
4
5 s1 object;
6
7 void g(void *t) {
8 int x;
9 s1 *p;
10
11 p = (s1 *)t;
12 x = p->x1; // x should be assigned value 5 but p->x1 is full-range
13 }
14
15 void main(void) {
16 s1 * p;
17
18 object.x1 = 5;
19 p = &object;
20 g((void *)p); // p cast as void pointer
21 }
x должно быть присвоено значение 5. Однако программное обеспечение принимает, что p->x1 имеет полную область значений значений, допускаемых его типом.