by fcambus on 6/22/22, 6:12 AM with 9 comments
by rgovostes on 6/22/22, 6:55 AM
It may be dated by now but there is also a tutorial on writing checkers (https://clang-analyzer.llvm.org/checker_dev_manual.html), or follow one of the many examples in the codebase.
My first checker is still there — it just turned 10 years old, and is under 100 lines without comments. https://github.com/llvm/llvm-project/blob/main/clang/lib/Sta...
by yaantc on 6/22/22, 8:14 AM
As said, there are few false positives. For embedded software the fact that Z3 understand bitfields and bit operations is nice. But in general we found that it makes better use of CTU information than a proprietary tool we're using (and now consider phasing out).
When used with cross compiled software the CC+ClangSA combination can be made to work, but is sometimes a bit rough when there are GCC/Clang subtle incompatibilities. But nothing too bad, and CC provided the hooks to work around any issue we found.
Even in "verification" mode, Z3 also helps the analysis as I understand from the docs. Some cheap Z3 analysis are used to prune some paths, which also helps the classical range analysis. Those tools must make some approximation to deal with the combinatorial explosion, so pruning useless paths early can help exploring others leading to bugs. So Z3, even in the default mode, is not only to filter out false positive but can also help finding issues.
I would highly recommend it for people using C and C++. With those languages the tooling around is very important to (partially) mitigate their known "dangerosity".
by fallingmeat on 6/22/22, 7:49 AM
by zogomoox on 6/22/22, 1:35 PM