[asveikau]

Looking at the categories of warnings it produces, I'm not surprised. When I've used similar tools trying to detect the same things, I also saw false positives. It's probably not an easy set of problems, otherwise we'd have it built-in to more tools and enabled by default.

[rwmj]

We routinely run nbdkit through Coverity and it finds bugs, although it too has false positives. Also the reports produced by Coverity are really nice - long enough to tell you where the bug is, but not too long to be overwhelming.

I've been meaning to formally prove one of our internal "mini libraries" using Frama-C. If we did that then no one would be able to complain about bugs in it :-)