Type checks in Frama-c

Question

I would like to know if Frama-C implements some sort of type checking associated to pointers. For instance, consider the following:

int x[10];
void * v = x;

//@ assert isOfTypeInt(x, 10)
//@ assert isOfTypeInt(v, 10) 

Is there anything similar to the above in spirit?

Looking at the ACSL manual, there are many ways to check the use of memory and pointers (part of which are implemented in Frama-C Oxygen). I haven't found any general support to handle type information though. Is there a frama-c plugin we can use for this purpose?

Thanks, Eduardo

Answer 1

There is indeed no such thing in ACSL. In fact, memory locations in C do not really have type information tied to them: if we ignore potential alignment constraints, any block of 4 bytes can be used to store a 32-bit integer.

That said, Frama-C is an extensible platform and it's always possible to write a plug-in for specific needs. For plain variables such as x in your example, the declared type is directly accessible in the vtype field of the corresponding varinfo in the AST. For pointers, such as v, it should be possible to exploit Value's results to see where they might point to and use this to derive appropriate type information (the main issue being to decide what should be done when Value is imprecise and gives several potential locations with different types).