[PATCH] D54978: Move the SMT API to LLVM

Thu Feb 7 09:45:26 PST 2019

brzycki added a comment.

This commit is causing a build-break for our nightly cross compilers of arm and aarch64. The immediately preceding commit of D54977 <https://reviews.llvm.org/D54977> does not break with the exact same invocation.

The problem is our build machine (Ubuntu 18.04 LTS) installs an old version of Z3 that is incompatible with LLVM's tip of tree. To deal with this we add `-D CLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF` to force disabling Z3 even if CMake detects the library is installed.

With this patch I am unable to disable Z3 because `CLANG_ANALYZER_ENABLE_Z3_SOLVER` is no longer in the codebase and setting `-D LLVM_ENABLE_Z3_SOLVER=OFF` still builds Z3 support (which fails):

  [74/187] Building CXX object lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
  /usr/bin/clang++-6.0  -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Support -I/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support -I/usr/include/libxml2 -Iinclude -I/tmp/tmp.UCDOJjmgJ1/src/llvm/include -fPIC -fvisibility-inlines-hidden -Werror=date-time -Werror=unguarded-availability-new -std=c++11 -Wall -Wextra -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wmissing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough -Wcovered-switch-default -Wno-noexcept-type -Wnon-virtual-dtor -Wdelete-non-virtual-dtor -Wstring-conversion -fdiagnostics-color -ffunction-sections -fdata-sections -O3 -DNDEBUG    -fno-exceptions -fno-rtti -MD -MT lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp
  /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp:44:40: error: no matching function for call to 'Z3_get_error_msg'
                             llvm::Twine(Z3_get_error_msg(Context, Error)));
                                         ^~~~~~~~~~~~~~~~

Repository:
  rC Clang

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

https://reviews.llvm.org/D54978