This kind of code is beyond current Frama-C/WP capabilities. Basically, the main (industrial) use-cases of Frama-C/WP are generally programs with strongly constrained coding rules. Such codes are generally well-typed and use very few operations on bits. Consequently, heterogeneous casts, unions and bit operation have a poor support in Frama-C/WP.

Here are the properties that are intractable:

• the link between the values read as char and read as size_t,
• the fact that extracting 8 bits at some location is the extraction of a byte.

There is currently ongoing research effort to deal with the first problem, that will probably need additional R&D effort on industrial use cases to be fully scalable.

On the second aspect, to the best of my knowledge, there have been questions along years on this topic, but no industrial will to improve this feature in WP.