fre 2018-06-22 klockan 19:34 +0000 skrev 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 <ffmpeg-devel@ffmpeg > > .org> > > Subject: Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of- > > concept (kinda) > > > > > 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. > > > > You're right, I missed that, but now that I see it - it's not > redundant, it's just wrong. > It's perfectly ok for an arbitrary atom to have size smaller than 8 > bytes (frma is, for example, > only 4 bytes), it's not ok for the two specific atoms that we're > parsing - stco & co64. > The validation of size >= 8 already existed in all branches that > required it > (parse_atoms / update_stco_offsets / update_co64_offsets) > > > > 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. > > > > > 2. this extra statement - 'pos = atom->data + 8 + 4*i;' - > > > why for on 'i' when we only care about 'pos'? > > > > It's an attempt at making that code easier to prove. If I can > > convince alt-ergo that atom_data[0..(atom_size-1)] is valid and > > that the code only touches bytes in that range then the code will > > pass inspection. > > Using end-pos for that ended up with some rather torturous ACSL > > annotations. > > > > > 3. this code - 'current_offset = ((uint64_t)current_offset + > > > (context->moov_atom_size & 0xFFFFFFFF)) & 0xFFFFFFFF;' > > > why go through 64 bit when we later cast it to 32 bit? > > > > Yeah that's just my attempt at saying "relax, overflow is fine". > > Judging by the ACSL manual [1], adding an explicit cast to uint32_t > > may be enough. > > > > Sounds a bit problematic to me to demand that everyone here learn all > this stuff now, > but again, it's not my call...
I wouldn't demand everyone do this, but I might want it for stuff I maintain. /Tomas _______________________________________________ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
