Язык C позволяет использование операторов, которые снимают переменную в качестве пустого указателя. Верификация However, 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
позволил полный спектр значений его тип.