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

[Tomas Härdin]

tor 2024-05-16 klockan 13:12 +0100 skrev 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

They could easily be incorporated into FATE or a post-commit hook

> * their output doesn't get boring

The output of Frama-C in general tends to be quite chatty. I've asked a
couple of time for them to add exit codes, for example returning with
zero only if there are no alarms and no unproven proof obligations.
With Eva grepping for " 0 alarms generated by the analysis." is one
way, but that's also quite ugly

/Tomas