Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-23 Thread Michael Niedermayer
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

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-23 Thread Tomas Härdin
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

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-23 Thread Tomas Härdin
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

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-22 Thread 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 (atom.size < atom.header_size)'. > > atom.header_size is either 8 or 16,

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-22 Thread Eran Kornblau
> -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

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-22 Thread Tomas Härdin
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

Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-22 Thread Eran Kornblau
> 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

[FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

2018-06-22 Thread Tomas Härdin
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