On Sat, Jun 23, 2018 at 11:40:52AM +0200, Tomas Härdin wrote:
> fre 2018-06-22 klockan 23:12 +0200 skrev Michael Niedermayer:
> > On Fri, Jun 22, 2018 at 04:51:09PM +0200, Tomas Härdin wrote:
> > > fre 2018-06-22 klockan 14:07 + skrev Eran Kornblau:
> > > > First, regarding the if you added, it
tches > .org>
> > Subject: Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-
> > concept (kinda)
> >
> > > fre 2018-06-22 klockan 14:07 + skrev Eran Kornblau:
> > > First, regarding the if you added, it's redundant - if y
fre 2018-06-22 klockan 23:12 +0200 skrev Michael Niedermayer:
> On Fri, Jun 22, 2018 at 04:51:09PM +0200, Tomas Härdin wrote:
> > fre 2018-06-22 klockan 14:07 + skrev Eran Kornblau:
> > > First, regarding the if you added, it's redundant - if you look a few
> > > lines above, you'll see 'if (a
On Fri, Jun 22, 2018 at 04:51:09PM +0200, Tomas Härdin wrote:
> fre 2018-06-22 klockan 14:07 + skrev Eran Kornblau:
> > First, regarding the if you added, it's redundant - if you look a few lines
> > above, you'll see 'if (atom.size < atom.header_size)'.
> > atom.header_size is either 8 or 16,
> -Original Message-
> From: ffmpeg-devel [mailto:ffmpeg-devel-boun...@ffmpeg.org] On Behalf Of
> Tomas Härdin
> Sent: Friday, June 22, 2018 5:51 PM
> To: FFmpeg development discussions and patches
> Subject: Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of
fre 2018-06-22 klockan 14:07 + skrev Eran Kornblau:
> First, regarding the if you added, it's redundant - if you look a few lines
> above, you'll see 'if (atom.size < atom.header_size)'.
> atom.header_size is either 8 or 16, it can't be anything else, so atom.size
> can't be < 8 at this point
> Hi
>
> I've recently been looking at formal proof systems for minimizing bugs.
> One common example is SPARK, which is an Ada variant which uses contracts,
> guaranteed termination and lack of dynamic allocation to make reasoning about
> SPARK programs much easier. This allows automatic checki
Hi
I've recently been looking at formal proof systems for minimizing bugs.
One common example is SPARK, which is an Ada variant which uses
contracts, guaranteed termination and lack of dynamic allocation to
make reasoning about SPARK programs much easier. This allows automatic
checking for things