brzycki added a comment.

In D54978#1395288 <https://reviews.llvm.org/D54978#1395288>, @ddcc wrote:

> In D54978#1395268 <https://reviews.llvm.org/D54978#1395268>, @brzycki wrote:
>
> > I think I found why others are struggling to recreate this issue. I did not 
> > have the package `z3/bionic` installed. This provides the `/usr/bin/z3` 
> > executable which `llvm/cmake/modules/FindZ3.cmake` relies upon to determine 
> > the correct `Z3_VERSION_STRING`.
>
>
> Yeah, that's what I meant by best-effort only. Due to upstream Z3's design, 
> without the binary, there is no easy way to retrieve the current installed 
> version, so when I originally wrote the Z3 integration, it seemed fine to let 
> the version check pass. Given the issues that have come up, it might make 
> more sense to at least emit a warning, or explicitly fail if the version 
> can't be determined, and prompt the user to install the binary.


Hello @ddcc.
I agree with your reasoning here and developed a patch based on this line of 
thought:

  diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
  index 5c6d3f0b427..b213342df37 100644
  --- a/llvm/cmake/modules/FindZ3.cmake
  +++ b/llvm/cmake/modules/FindZ3.cmake
  @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
       string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
              Z3_VERSION_STRING "${libz3_version_str}")
       unset(libz3_version_str)
  +else()
  +    # The version could not be determined from running Z3_EXECUTABLE. Set the
  +    # version Z3 to the lowest possible value such that all checks for a
  +    # minimum version will fail.
  +    set(Z3_VERSION_STRING "0.0.0")
   endif()
  
   # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if

This works for everything I could throw at it. If you think it's reasonable I 
can open another ticket and have the code reviewed as a separate fix.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978



_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to