[FFmpeg-devel] [PATCH] lavu/mem: Add av_fast_recalloc(), formally verify *size

[Tomas Härdin]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-lavu-mem-Add-av_fast_recalloc-formally-verify-size.patch
Type: text/x-patch
Size: 6577 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20220617/2e9cbdff/attachment.bin>