> An embedded C developer I've talked with quite often on some other forum,
> who imho is quite competent, said that Coverity is a poor tool that
> generates way too much false negatives and overlooks at the same time
> glaring issues. He was not happy about it. Said that's mostly an issue
> with all OpenSource tools for static C analysis. OTOH the commercial ones
> are very expensive usually, with a target market of critical things like
> aviation of safety systems in cars and military use, places where they
> spend billions on projects. Nothing there for the average company, and
> especially not for (frankly often underfunded) OpenSource projects.

I don't have any experience with Coverity, but used another commercial
static analyzer (SA) that I won't name in case there are similar legal
limitations as with Coverity ;)

With the commercial tool I have the same problem you mention: too many
false alarms. Most reports are a waste of time really. In the end, people
tend to ignore the tool.

The best results I get with Clang SA, used through CodeChecker. Very few
false alarms, and usually at least code smells. It's not sound of course,
but is free and could spot a few nasty bugs. I recommend trying CC+ClangSA.

One important point is the ability to do cross files analysis. It is very
common to use a value from a function in another file. With a "one file at
a time" analysis no assumption can be made on this value range, so the
analyzer must be conservative. This leads to a lot of false alarms in
practice.

With cross file analysis (called "cross translation units" or CTU analysis
in Clang SA), the SA can propagate constraints along paths traversing
multiple files. This makes a huge difference in my experience. As I
explained in another comment, this is well suited for an application: all
paths come from `main`. For a library the result will depend on the test
application(s) provided to the SA: the call to the library under test must
cover all the function domains for the analysis not to miss some issue.
Otherwise, it may use too restrictive constraints from the UT that are not
relevant to real life use.

But it may not be enough: the commercial tool I use do make cross file
analysis. It seems more limited than Clang SA though, and misses a lot.

Another thing that help IMHO is the use of Z3 as a checker. ClangSA uses a
simple and fast range based analysis. As far as SA goes, this is a bit
primitive and not as powerful as polyhedral analysis for example (which is
more expensive).

But when Clang SA range analysis finds an issue, it is cross checked with
the Z3 SMT solver, which can deal with more complex constraints, and
possible rejected there. I do embedded development, and Z3 can understand
bit fields and bit operations for example (trivial for a SMT solver with
bit vectors). I never tried with and without using Z3 in this way, but I
assume it helps.

In any case, I'm very happy with the results I get from ClangSA+CC with CTU
and Z3 enabled (check your LLVM toolchain for Z3 support, OK in Debian
stable for example). It's much better in practice than the costly
commercial tool we still use, for now.

For cross compilation, there may be a few Clang/GCC differences to
work-around. CodeChecker already handle some, but maybe not all. It's been
manageable in our case. For Linux based development CC should work fine out
of the box.