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

Wed Mar 31 07:06:22 PDT 2021

martong accepted this revision.
martong added a comment.

I went through the change and it looks good, seems like this is indeed a copy paste error from line 132.
I checked the related conversation, and thanks for all the effort spent with the test.

> 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?

This is a good fix, I'd like to see landed!

================
Comment at: clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c:6
+
+// Mock implementation: return UNDEF for the 5th invocation, otherwise it just
+// returns the result of the real invocation.
----------------
It's not clear why we have to wait for the 5th invocation. Can't we return UNDEF for the first time? That would eliminate the need to call the originalFN. 

By the way why do we have call the original, can't we just return immediately with Z3_L_TRUE?

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

https://reviews.llvm.org/D83660