How to enable Z3 cross check on clang-tidy

Clang Frontend clang-tidy
1

Hi, clang analyzer has a crosscheck-with-z3 config to reduce false positives. But I failed to enable it when using clang-tidy instead of clang directly. Is there a way to enable cross-check with z3 on clang-tidy?

Thanks.

2

To the best of my understanding, there is currently no way of specifying neither Static Analyser-level (basically, the “engine” or process itself) nor check-level configuration options if CSA is run within/through Tidy. You could try using scan-build to drive CSA (and then keep driving Tidy separately), or CodeChecker to drive both.

3

I think I managed to enable crosscheck-with-z3 with following parameters:

-Xclang -analyzer-config -Xclang crosscheck-with-z3=true

I’m not 100% confirm about this because my clang-tidy will crash when it try to call z3 solver. But I think this means the crosscheck has been enabled.