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 _______________________________________________ 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".