[PATCH] D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

Wed Mar 31 08:55:04 PDT 2021

OikawaKirie added a comment.

In D83660#2661369 <https://reviews.llvm.org/D83660#2661369>, @martong wrote:

>> BTW, I was obstructed by the z3 requirement in the regression test case when I tried to understand your test case. Even though I set the variables LLVM_Z3_INSTALL_DIR and LLVM_ENABLE_Z3_SOLVER during CMake, and the CSA can be correctly compiled with Z3, I still cannot make the test case run during make check-all. Therefore, this case was manually executed with llvm-lit -DUSE_Z3_SOLVER=1. Could you please tell me how to enable Z3 during llvm-lit.
>
> I am a bit unhappy that we cannot run the test automatically, but maybe in the future.
> @steakhal, https://reviews.llvm.org/D83677 seems to be related, should we push that?

I am just reporting this phenomenon and I am not sure whether it is caused by my bad configurations.
Under my configurations, the last step of `make check-all` will execute `llvm-lit` with argument `--param USE_Z3_SOLVER=0`, which will make all test cases requiring z3 skipped.
Although, clang is built with z3 under this configuration.

Can we automatically enable all test cases requiring z3 if clang is built with z3? I do not think the patch D83677 <https://reviews.llvm.org/D83677> really make the problem fixed.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83660/new/

https://reviews.llvm.org/D83660