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 5E2AB4AC20 for ; Thu, 16 May 2024 12:13:02 +0000 (UTC) Received: from [127.0.1.1] (localhost [127.0.0.1]) by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id A403968D47A; Thu, 16 May 2024 15:12:59 +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 1677A68C0C3 for ; Thu, 16 May 2024 15:12:53 +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 1s7Zye-004sH8-0n for ffmpeg-devel@ffmpeg.org; Thu, 16 May 2024 13:12:52 +0100 Date: Thu, 16 May 2024 13:12:51 +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: <42af1d43261e04d99171c93ed26947712e263be8.camel@haerdin.se> 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 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 * their output doesn't get boring One simple way to meet both criteria would be a cron job that runs overnigh= t, and messages the ML with just the issues that didn't exist in yesterday's r= un. Plenty of other ways to do it, but something like that would be a great sta= rt. _______________________________________________ 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".