[FFmpeg-devel] [WIP] False positives on Coverity

[Tomas Härdin]

tis 2024-05-14 klockan 14:28 +0300 skrev Rémi Denis-Courmont:
> 
> 
> Le 14 mai 2024 10:37:20 GMT+03:00, "Tomas Härdin" <git at haerdin.se> a
> écrit :
> > Formal methods would be better than the heuristics coverity uses.
> 
> That sounds like wishful thinking, or at least a distant pipe dream.
> Lets stick to what is possible and realistic today, please.

WP is a pipe dream yes, but Eva is quite near being practical. We can
add test entrypoints protected by #defines for various modules in the
codebase. lavu comes to mind. I might submit a patchset for this as a
conversation starter.

> And I don't think that it would be reasonable to require that every
> FFmpeg developer be able to update the hypothetical formal proofs
> whenever they make a code change.

I think this entirely depends. Much like we don't allow breaking FATE,
there is no reason to allow breaking low-level stuff covered by ACSL
contracts. For example if the AVRational functions are given a valid
rational (positive den), they should return a valid rational as well.

I should add that Eva can produce false positives as well. This can be
avoided to some extent by giving it less gas when developing and more
in FATE.

/Tomas