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" <g...@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 _______________________________________________ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org https://ffmpeg.org/mailman/listinfo/ffmpeg-devel To unsubscribe, visit link above, or email ffmpeg-devel-requ...@ffmpeg.org with subject "unsubscribe".