[PATCH] D106131: Fix FindZ3.cmake to support static libraries and Windows

Mon Jul 26 01:07:42 PDT 2021

tomasz-kaminski-sonarsource added inline comments.

================
Comment at: llvm/cmake/modules/FindZ3.cmake:17
   # The program that will be executed to print Z3's version.
-  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
+  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
        "#include <assert.h>
----------------
steakhal wrote:
> Do you need to change it to `cpp`?
Yes, for static version of z3, it's need to be linked with C++ runtime. Changing extension is the easiest way to signal cmake that this is meant to be C++ code.

================
Comment at: llvm/cmake/modules/FindZ3.cmake:101-102
        z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
-  string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1"
+  string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]).*$" "\\1"
          Z3_BUILD "${z3_version_str}")

----------------
steakhal wrote:
> Oh, so it never matched. What is the purpose of this in that case?
> If we did not recognize this sooner, I mean...
If major.minor is greater than required (e.g. 4.8) the test passes despite ending up with "#define Z3_BUILD_NUMBER    11" as patch number, so once Z3 got minor updated, this does not cause issues.

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

https://reviews.llvm.org/D106131