I'd never heard of this cclyzer tool, thanks for sharing. This looks really interesting. Know of any other tools for C/C++/JVM static analysis that folks might not be aware of?

At the moment, I use GCC's -fanalyzer, the LLVM sanitizers + static analyzer, FB's Infer, and PVS Studio.

https://github.com/kframework/c-semantics while you can do static analysis with this the dynamic instrumentation of UB isnfar more thorough than ubsan