search

llvm / llvm-project

The LLVM Project is a collection of modular and reusable compiler and toolchain technologies.
http://llvm.org
Other
28.48k stars 11.77k forks source link

Trunk doesn't build with libz3-dev of ubuntu 18.04 #39475

Closed pmatos closed 4 years ago

pmatos commented 5 years ago
Bugzilla Link 40128
Resolution FIXED
Resolved on Jan 20, 2020 10:59
Version trunk
OS Linux
CC @devincoughlin,@mikhailramalho

Extended Description

Start a docker machine with ubuntu 18.04. Install libz3-dev and compile llvm/clang trunk with: cmake -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON -G Ninja ../llvm

You'll get from clang FAILED: tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/clangStaticAnalyzerCore.dir/Z3ConstraintManager.cpp.o /usr/bin/c++ -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -DSTDC_CONSTANT_MACROS -DSTDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Itools/clang/lib/StaticAnalyzer/Core -I/root/llvm/tools/clang/lib/StaticAnalyzer/Core -I/root/llvm/tools/clang/include -Itools/clang/include -Iinclude -I/root/llvm/include -fPIC -fvisibility-inlines-hidden -Werror=date-time -std=c++11 -Wall -Wextra -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough -Wno-maybe-uninitialized -Wno-class-memaccess -Wno-noexcept-type -Wdelete-non-virtual-dtor -Wno-comment -fdiagnostics-color -ffunction-sections -fdata-sections -fno-common -Woverloaded-virtual -fno-strict-aliasing -fno-exceptions -fno-rtti -MD -MT tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/clangStaticAnalyzerCore.dir/Z3ConstraintManager.cpp.o -MF tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/clangStaticAnalyzerCore.dir/Z3ConstraintManager.cpp.o.d -o tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/clangStaticAnalyzerCore.dir/Z3ConstraintManager.cpp.o -c /root/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp /root/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp: In function 'void {anonymous}::Z3ErrorHandler(Z3_context, Z3_error_code)': /root/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:49:57: error: cannot convert 'Z3_context' {aka '_Z3_context'} to 'Z3_error_code' llvm::Twine(Z3_get_error_msg(Context, Error))); ^~~ In file included from /usr/include/z3.h:26, from /root/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:23: /usr/include/z3_api.h:5314:53: note: initializing argument 1 of 'const char Z3_get_error_msg(Z3_error_code)' Z3_string Z3_API Z3_get_error_msg(Z3_error_code err);



My guess is that cmake needs a stricter check for the version of libz3.
mikhailramalho commented 4 years ago

The latest version of the FindZ3.cmake will refuse to configure if Z3 is < 4.7.1.

Unfortunately, the Z3 version shipped with Ubuntu is quite old.

pmatos commented 5 years ago

assigned to @devincoughlin