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

[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 ...

If you compare the time it takes a human to anotate a piece of code (some of
this anotation itself may be incorrect) and subsequently a analyzer to find bugs.
To the alternative
of a human manually reviewing the code line by line and a analyzer running over
the code which does not need anotations

which finds more bugs ?
The question matters, because i think we want the maximum return for the time that
is invested


[...]

-- 
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/20180622/ef830949/attachment.sig>