I am wondering how difficult it would be to add rudimentary support for something like sizeof T[n] (which to my knowledge is an explicit C construct for a dynamically-sized array).

My experiments so far have shown that it is not supported (well?) in Frama-C. So my questions are: What would be required to implement it, in any capacity? What about kernel support? What about the development of an analysis domain for Eva?

I am willing to invest a modest amount of effort into developing a solution (if it is feasible). So far I have consulted much of the documentation available on the Frama-C website; it is, however, conceivable that I’ve missed some crucial details regarding where to start.