4 ms·

> > The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm work

by yaantc 4y ago

> > The Clang static analyzer [1], used through CodeChecker (CC) [2], do support CTU (enabled with `--ctu`). I'm very happy with the result on the code I'm working on. > I have done some preliminary testing with this on the OpenZFS codebase and I am less than happy with the result [...] A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu. I would expect the lack of Z3 support to lead to a lot more false alarms in a FS, as the analysis with only the Clang SA build it range analysis will be basic and won't understand anything related to bit fields and operations for example. The `llvm` package must depend on a `libz3-4` package, recent enough (on Bookworm it's 4.8.10, but IIRC anything >= 4.7 would be used). Another way to check could be to use the CodeChecker `--z3-refutation`: this is enabled by default if LLVM has the Z3 support, but if requested explicitly should fail if not (untried, TBC).

ryao 4y ago
> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu. That was one of the first things I did. Recompiling with z3 support made little difference. That said, I thought --z3-refutation Was the default when it was available. I will try rerunning tests with it explicitly specified, but I do not expect much from that, since running tests with --z3, which replaces the range checker with z3, did not really eliminate reports beyond those that were in files that caused clang’s static analyzer to crash when that was set.
- yaantc 4y ago
  Yes, if the LLVM toolchain has Z3 support then `--z3-refutation` will be the default. It's only useful if you want an error in case the LLVM toolchain may not have this support. I've read somewhere that the "full Z3" mode with `--z3` is very experimental and not well maintained. It didn't crash when I tried it but was no better and way too slow: typically 15 times slower on average, but a few files took over 24 hours to check.

by yaantc 4y ago

ryao 4y ago

> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu. That was one of the first things I did. Recompiling with z3 support made little difference. That said, I thought --z3-refutation Was the default when it was available. I will try rerunning tests with it explicitly specified, but I do not expect much from that, since running tests with --z3, which replaces the range checker with z3, did not really eliminate reports beyond those that were in files that caused clang’s static analyzer to crash when that was set.

yaantc 4y ago
Yes, if the LLVM toolchain has Z3 support then `--z3-refutation` will be the default. It's only useful if you want an error in case the LLVM toolchain may not have this support. I've read somewhere that the "full Z3" mode with `--z3` is very experimental and not well maintained. It didn't crash when I tried it but was no better and way too slow: typically 15 times slower on average, but a few files took over 24 hours to check.