[FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin (and an UB fix)

[Tomas Härdin]

Hi

So as I said in the coverity thread it would be good if we could get at
least part of the codebase covered using formal tools. To this effect I
sat down for an hour just now and gave libavutil/common.h a go with
Frama-C's Eva plugin [1;2]. This plugin performs value analysis, which
is a much simpler analysis compared to say the weakest predicate (WP)
plugin.

Going through the functions from top to bottom it only took until
av_clipl_int32_c() to find my first UB, a patch for which is attached.
Thus my harping on this has born at least some fruit.

To run the analysis implemented in this set of patches (all of which
I've attached here because I don't want to bother writing six follow-up
email), first install frama-c using opam. I'm using 28.0~beta (Nickel).
Then run "make verify" in libavutil/ and Eva should tell you that 33%
of functions are covered and 100% of statements in those functions are
covered, with zero alarms.

If the project isn't interested in this then I'll probably continue
fiddling with it on my own mostly as exercise. But I suspect it will
bear even more fruit in time.

/Tomas

[1] https://frama-c.com/
[2] https://frama-c.com/fc-plugins/eva.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-lavu-Very-basic-Eva-setup.patch
Type: text/x-patch
Size: 2694 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0002-eva-Add-av_log2_16bit.patch
Type: text/x-patch
Size: 1033 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0001.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0003-eva-av_clip.patch
Type: text/x-patch
Size: 918 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0004-eva-av_clip64.patch
Type: text/x-patch
Size: 1073 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0003.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0005-eva-av_clip_.patch
Type: text/x-patch
Size: 635 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0006-lavu-common.h-Fix-UB-in-av_clipl_int32_c.patch
Type: text/x-patch
Size: 972 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0005.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0007-eva-av_clipl_int32.patch
Type: text/x-patch
Size: 557 bytes
Desc: not available
URL: <https://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20240515/4fb16bec/attachment-0006.bin>