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).