Assumptions About Variables Cast as Void Pointers

The C language allows the use of statements that cast a variable as a void pointer. However, Polyspace^® verification of these statements entails a loss of precision.

Consider:

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  }

On line 12, the variable x must be assigned the value 5. However, the software assumes that p->x1 has full range of values allowed by its type.