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

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

The point is to let the machine automatically catch when certain
assumptions are violated, since mistakes happen. You are correct that
it can take considerable time though. I wouldn't insist on anyone else
doing it, this is mostly for my own sanity. And of course if the
contracts are wrong then you're screwed. Just like if ones assumptions
of what a function does are wrong.

As an example of just how wordy these annotations can get, I've
attached binary_search_tree_proved.c from [1]. It's 8 lines of code and
over 100 lines of annotations. But it does prove correct.

To cap off this post, I'll link to what I've said on the 'ol blogaroo
about Ada/SPARK: http://härdin.se/blog/2018/01/20/trying-out-ada-spark/

/Tomas

[1] https://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=mantis:fra
ma-c:tutorial:lifo-2014:solutions.tar.gz
-------------- next part --------------
A non-text attachment was scrubbed...
Name: binary_search_tree_proved.c
Type: text/x-csrc
Size: 3346 bytes
Desc: not available
URL: <http://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20180623/f56a036b/attachment.c>