Taking a stab at formally verifying some small part of #FFmpeg (libavutil/common.h), but my efforts are immediately thwarted by bithacks like this: if (a&(~0xFF)) return (~a)>>31;
That clamps an int to [0,255]. If it's hard to tell, don't worry; the weakest predicate and value analysis plugins in frama-c can't make much sense of it either