I think it's best to send this as a separate patch. I also took some
time yesterday evening to formally verify the size computation because
it relying on overflow irked me. Doing the same with av_fast_realloc()
and av_fast_recalloc() themselves is rather more involved and probably
requires a newer version of frama-c because 20.0 does not support
verifying allocations.

For the uninitiated the lemmas are there to help the provers along. The
/*@ ... */ quote before compute_size() is its contract.

I also now guarantee that av_fast_recalloc() sets *size to a multiple
of elsize, and the size is also such a multiple except when nelem == 0.

/Tomas