[PATCH] D54391: Fix compatibility with z3-4.8.1

Jan Kratochvil via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Sun Nov 11 05:48:02 PST 2018


jankratochvil created this revision.
jankratochvil added a reviewer: clang.
jankratochvil added a project: clang.

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)));
                                          ^~~~~~~~~~~~~~~~~~~
                                          Z3_get_error_msg

clang CMakeLists.txt has:

  find_package(Z3 4.7.1 EXACT)

Despite cmake documentation <https://cmake.org/cmake/help/v3.11/command/find_package.html#version-selection> 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/libz3.so (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);
  }


Repository:
  rC Clang

https://reviews.llvm.org/D54391

Files:
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp


Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -46,7 +46,7 @@
 // Function used to report errors
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
   llvm::report_fatal_error("Z3 error: " +
-                           llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
+                           llvm::Twine(Z3_get_error_msg(Context, Error)));
 }
 
 /// Wrapper for Z3 context


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D54391.173555.patch
Type: text/x-patch
Size: 575 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20181111/429d7ff1/attachment.bin>


More information about the cfe-commits mailing list