[FFmpeg-devel] [PATCH 09/13] avcodec/elbg: Also allocate buffers for recursion only once

[Tomas Härdin]

fre 2021-09-17 klockan 04:08 +0200 skrev Andreas Rheinhardt:
> This is possible because the number of elements needed in each
> recursion step decreases geometrically, so the geometric series
> provides an upper bound for the sum of number of elements of
> the needed buffers.

Looks like a thing that could be verified formally via Frama-C. I might
do this at some point.

/Tomas