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
struct tree { int data;
struct tree* left;
struct tree* right; };
/*@ inductive reachable{L}(struct tree* t1, struct tree* t2) {
case single: \forall struct tree* t; reachable(t,t);
case transl: \forall struct tree* t1,*t2; reachable(t1->left,t2) ==>
reachable(t1,t2);
case transr: \forall struct tree* t1, *t2;
reachable(t1->right,t2) ==> reachable(t1,t2);
}
*/
/*@ lemma reachable_trans_l:
\forall struct tree *t1, *t2;
reachable(t1,t2) && \valid(t2) ==> reachable(t1, t2->left);
*/
/*@ lemma reachable_trans_r:
\forall struct tree *t1, *t2;
reachable(t1,t2) && \valid(t2) ==> reachable(t1, t2->right);
*/
/*@ predicate well_formed{L}(struct tree* t) =
\forall struct tree* t1; reachable(t,t1) ==>
\valid(t1) || t1 == (struct tree*)0;
*/
/*@ predicate contains{L}(struct tree* t, int data) =
\valid(t) &&
\exists struct tree* t1; \valid(t1) && reachable(t,t1) && t1->data == data;
*/
/*@ inductive sorted_tree{L}(struct tree* t) {
case empty{L}: sorted_tree((struct tree*)0);
case full{L}: \forall struct tree* t; well_formed(t) &&
\valid(t) && sorted_tree(t->left) && sorted_tree(t->right) &&
(\forall struct tree* t1; reachable(t->left, t1) ==> t->data >= t1->data) &&
(\forall struct tree* t1; reachable(t->right, t1) ==> t->data <= t1->data) ==>
sorted_tree(t);
}
*/
/*@ lemma sorted_tree_projl:
\forall struct tree* t, *t1;
sorted_tree(t) && \valid(t) && \valid(t1) && reachable(t->left,t1) ==>
t1->data <= t->data;
*/
/*@ lemma sorted_tree_projr:
\forall struct tree* t, *t1;
sorted_tree(t) && \valid(t) && \valid(t1) && reachable(t->right,t1) ==>
t1->data >= t->data;
*/
/*@ lemma sorted_children:
\forall struct tree* t;
\valid(t) && sorted_tree(t) ==> sorted_tree(t->left) && sorted_tree(t->right);
*/
/* @ lemma reachable_choice{L}:
\forall struct tree* t, *t1;
\valid(t) && \valid(t1) && well_formed(t) && reachable(t,t1) ==>
t == t1 || reachable(t->left, t1) || reachable(t->right,t1);
*/
/*@ lemma contains_choice{L}:
\forall struct tree* t; \forall int data;
\valid(t) && contains(t,data) ==>
t->data == data || contains(t->left, data) || contains(t->right, data);
*/
/*@
requires sorted_tree(t);
requires well_formed(t);
assigns \nothing;
behavior find:
assumes contains(t,key);
ensures \valid(\result);
ensures \result->data == key;
behavior not_find:
assumes !contains(t,key);
ensures \result == (struct tree*)0;
complete behaviors;
disjoint behaviors;
*/
struct tree* search(int key, struct tree* t) {
struct tree* current = t;
/*@
loop invariant reachable(t,current);
loop invariant well_formed(current);
loop invariant sorted_tree(current);
loop invariant contains(t,key) <==> contains(current,key);
loop assigns current;
*/
while (current) {
//@ assert \valid(current);
if (current->data == key) return current;
if (current->data < key)
/*@ assert \forall struct tree* t1;
\valid(t1) && reachable(current->left,t1) ==> t1->data < key; */
//@ assert !contains(current->left,key);
current = current->right;
else
//@ assert !contains(current->right,key);
current = current -> left;
}
return current; }
/*
Local Variables:
compile-command: "frama-c-gui -wp -wp-rte binary_search_tree_proved.c"
End:
*/
_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
