Clang Static Analyzer and the Z3 constraint solver
As far as static analyzers are concerned, one of the most important point to consider is filtering out false positives as much as possible, in order for the reports to be actionable.
This is an area on which Coverity did an excellent job, and likely a major reason why they got so popular within the open source community, despite being a closed-source product.
The option is enabled in the Debian 11 package (clang-tools-11), but not in Fedora 36 or Ubuntu 22.04 ones. I added a build option (not enabled by default) to the llvm and clang packages in Pkgsrc, and successfully built Z3 enabled packages on NetBSD.
There are two ways of using Z3 with the Clang Static Analyzer, and to demonstrate them, let’s reuse the small demo snippet from the SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer paper.
This is a lot slower than the default, and the commit which documented the feature mentions a ~15x slowdown over the built-in constraint solver.
