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

[Andrew Sayers]

On Wed, May 15, 2024 at 09:39:43PM +0200, Tomas Härdin wrote:
> 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

I'm all for automated checks, but in my experience they're only worthwhile
if two conditions are met:

* they run automatically on a regular basis
* their output doesn't get boring

One simple way to meet both criteria would be a cron job that runs overnight,
and messages the ML with just the issues that didn't exist in yesterday's run.

Plenty of other ways to do it, but something like that would be a great start.