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

[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 +0000 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.
> > > 
> > > If you look closely you'll see that check is after subtracting
> > > atom.header_size.
> > > 
> > > > I'll leave it to the maintainers to decide whether this tool is helpful or not, IMHO, all these comments make the 
> > > > code less readable, and some of the changes make it less efficient. I don't think this slight reduction of performance 
> > > > matters much in the context of faststart, but in other parts of ffmpeg it can be significant.
> > > > 
> > > > Few examples to why I think it's less efficient -
> > > > 1. the change of macros to functions - maybe the compiler will inline them, but maybe it won't...
> > > 
> > > You're assuming inlining actually makes the code faster. It's not the
> > > 80's anymore.
> > 
> > Until someone tests it, both claims are assumtations.
> > The date on the calender surely is not a good argument though even though it
> > has a somewhat "authorative" vibe to it.
> > 
> > Personally i prefer inline/always inline functions over macros when they are
> > equally fast though ...
> > 
> > Speaking about the date. I would have thought the need to manually annotate the
> > code for analyzers was a thing more for the past and for academia. But quite
> > possibly i have missed something ...
> 
> It's common in industries where you need to guarantee that a piece of
> code will never crash. Aerospace comes to mind.

If you want to make FFmpeg reach Aerospace / Medicine like levels of
bug-free-ness, that is welcome.

Thanks

[...]

-- 
Michael     GnuPG fingerprint: 9FF2128B147EF6730BADF133611EC787040B0FAB

Asymptotically faster algorithms should always be preferred if you have
asymptotical amounts of data
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: not available
URL: <http://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20180623/8473645b/attachment.sig>