From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org [79.124.17.100]) by master.gitmailbox.com (Postfix) with ESMTP id 417C54AC2C for ; Thu, 16 May 2024 12:54:51 +0000 (UTC) Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id 6398668D487; Thu, 16 May 2024 15:54:49 +0300 (EEST) Received: from alt2.a-painless.mh.aa.net.uk (unknown [81.187.30.51]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id 11E2968D119 for ; Thu, 16 May 2024 15:54:43 +0300 (EEST) Received: from 5.f.3.0.5.d.d.e.2.7.f.f.9.7.2.c.0.5.8.0.9.1.8.0.0.b.8.0.1.0.0.2.ip6.arpa ([2001:8b0:819:850:c279:ff72:edd5:3f5] helo=andrews-2024-laptop.sayers) by painless-a.thn.aa.net.uk with esmtp (Exim 4.96) (envelope-from ) id 1s7ad8-004wNi-0h for ffmpeg-devel@ffmpeg.org; Thu, 16 May 2024 13:54:42 +0100 Date: Thu, 16 May 2024 13:54:41 +0100 From: Andrew Sayers To: FFmpeg development discussions and patches Message-ID: References: <42af1d43261e04d99171c93ed26947712e263be8.camel@haerdin.se> MIME-Version: 1.0 Content-Disposition: inline In-Reply-To: Subject: Re: [FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin (and an UB fix) X-BeenThere: ffmpeg-devel@ffmpeg.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: FFmpeg development discussions and patches List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: FFmpeg development discussions and patches Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Errors-To: ffmpeg-devel-bounces@ffmpeg.org Sender: "ffmpeg-devel" Archived-At: List-Archive: List-Post: On Thu, May 16, 2024 at 02:31:31PM +0200, Tomas H=E4rdin wrote: > tor 2024-05-16 klockan 13:12 +0100 skrev Andrew Sayers: > > On Wed, May 15, 2024 at 09:39:43PM +0200, Tomas H=E4rdin 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 FATE is a good idea, but post-commit hooks break some workflows. For example, I like to start a test in one window, then put together a comm= it in another window. I can always amend the commit if there's a problem. The documentation suggests there are some hooks around e-mailing[1], but I haven't tried them. > = > > * 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 Yeah, IMHO the refusal to listen to such reasonable requests is the standard way for these projects to sabotage themselves. Diffing against the previous run tends to work a little better than grepping for a magic word, but still ugly, and you end up having to get rid of line numbers with `sed` or something. I find it's easier to put up with such hacks by constantly reminding myself: No code solution can ever be as ugly as having to do it all by hand. [1] https://git-scm.com/book/en/v2/Customizing-Git-Git-Hooks#_email_hooks _______________________________________________ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org https://ffmpeg.org/mailman/listinfo/ffmpeg-devel To unsubscribe, visit link above, or email ffmpeg-devel-request@ffmpeg.org with subject "unsubscribe".