Page MenuHomePhabricator

Fix compatibility with z3-4.8.1

Authored by jankratochvil on Nov 11 2018, 5:47 AM.



With z3-4.8.1 as found in Fedora Rawhide (future Fedora 30) as z3-devel-4.8.1-1.fc30.x86_64:

../tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp: In function 'void {anonymous}::Z3ErrorHandler(Z3_context, Z3_error_code)':
../tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:49:40: error: 'Z3_get_error_msg_ex' was not declared in this scope
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
../tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:49:40: note: suggested alternative: 'Z3_get_error_msg'
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));

clang CMakeLists.txt has:

find_package(Z3 4.7.1 EXACT)

Despite cmake documentation claims "If no such version file is available then the configuration file is assumed to not be compatible with any requested version." in reality cmake-3.12.2-1.fc30.x86_64 with z3-devel-4.8.1-1.fc30.x86_64 still does find it:

-- Found Z3: /usr/lib64/ (Required is exact version "4.7.1")

clang is using Z3_get_error_msg_ex(), already /usr/include/z3/z3_api.h of z3-devel-4.7.1-1.fc28.x86_64 states for it "Retained function name for backwards compatibility within v4.1" and it is implemented only as:

Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
    return Z3_get_error_msg(c, err);

Diff Detail


Event Timeline

jankratochvil created this revision.Nov 11 2018, 5:47 AM
ddcc accepted this revision.Nov 11 2018, 1:31 PM
ddcc added a subscriber: NoQ.
This revision is now accepted and ready to land.Nov 11 2018, 1:31 PM
This revision was automatically updated to reflect the committed changes.

Since we're supporting version 4.8.1 now, the cmake file should be changed to "minimum" instead of "exact".