From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <ffmpeg-devel-bounces@ffmpeg.org>
Received: from ffbox0-bg.mplayerhq.hu (ffbox0-bg.ffmpeg.org [79.124.17.100])
	by master.gitmailbox.com (Postfix) with ESMTP id ADC7F4AB7C
	for <ffmpegdev@gitmailbox.com>; Tue, 14 May 2024 07:37:35 +0000 (UTC)
Received: from [127.0.1.1] (localhost [127.0.0.1])
	by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTP id BD9C568D41F;
	Tue, 14 May 2024 10:37:31 +0300 (EEST)
Received: from glom.nmugroup.com (glom.nmugroup.com [193.183.80.6])
 by ffbox0-bg.mplayerhq.hu (Postfix) with ESMTPS id 501AB68D500
 for <ffmpeg-devel@ffmpeg.org>; Tue, 14 May 2024 10:37:25 +0300 (EEST)
Received: from localhost (localhost [127.0.0.1])
 by glom.nmugroup.com (Postfix) with ESMTP id 86AED5429BDB
 for <ffmpeg-devel@ffmpeg.org>; Tue, 14 May 2024 09:37:24 +0200 (CEST)
Received: from [10.10.150.6] (unknown [134.65.164.34])
 (Authenticated sender: git01)
 by glom.nmugroup.com (Postfix) with ESMTPSA id 4BDD45428C92
 for <ffmpeg-devel@ffmpeg.org>; Tue, 14 May 2024 09:37:20 +0200 (CEST)
Message-ID: <3a647bc5a15399b3217530566f05ee7d77b530db.camel@haerdin.se>
From: Tomas =?ISO-8859-1?Q?H=E4rdin?= <git@haerdin.se>
To: FFmpeg development discussions and patches <ffmpeg-devel@ffmpeg.org>
Date: Tue, 14 May 2024 09:37:20 +0200
In-Reply-To: <20240513233816.GL6420@pb2>
References: <20240513233816.GL6420@pb2>
User-Agent: Evolution 3.46.4-2 
MIME-Version: 1.0
Subject: Re: [FFmpeg-devel] [WIP] False positives on Coverity
X-BeenThere: ffmpeg-devel@ffmpeg.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: FFmpeg development discussions and patches <ffmpeg-devel.ffmpeg.org>
List-Unsubscribe: <https://ffmpeg.org/mailman/options/ffmpeg-devel>,
 <mailto:ffmpeg-devel-request@ffmpeg.org?subject=unsubscribe>
List-Archive: <https://ffmpeg.org/pipermail/ffmpeg-devel>
List-Post: <mailto:ffmpeg-devel@ffmpeg.org>
List-Help: <mailto:ffmpeg-devel-request@ffmpeg.org?subject=help>
List-Subscribe: <https://ffmpeg.org/mailman/listinfo/ffmpeg-devel>,
 <mailto:ffmpeg-devel-request@ffmpeg.org?subject=subscribe>
Reply-To: FFmpeg development discussions and patches <ffmpeg-devel@ffmpeg.org>
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Errors-To: ffmpeg-devel-bounces@ffmpeg.org
Sender: "ffmpeg-devel" <ffmpeg-devel-bounces@ffmpeg.org>
Archived-At: <https://master.gitmailbox.com/ffmpegdev/3a647bc5a15399b3217530566f05ee7d77b530db.camel@haerdin.se/>
List-Archive: <https://master.gitmailbox.com/ffmpegdev/>
List-Post: <mailto:ffmpegdev@gitmailbox.com>

Formal methods would be better than the heuristics coverity uses. At
the moment such methods are still too expensive for general use except
for the most safety critical applications (aerospace etc). But perhaps
in time the tooling and SMT solvers will improve sufficiently to make
it commonplace.

For FFmpeg the Eva and WP plugins for Frama-C would be of relevance.
I've been toying with the idea on and off

/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-request@ffmpeg.org with subject "unsubscribe".