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
