clang in official apt repo built without z3 support

Hello,

I am trying to run scan-build with crosscheck with z3 like:
scan-build-9 -o scan-report_cc -analyzer-config
'crosscheck-with-z3=true' make

Unfortunately the packages in then official repo here:
https://apt.llvm.org/

are build without Z3 support so I get:
fatal error: error in backend: Clang was not compiled with Z3 support,
rebuild with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON

Is there a reason for this? And is it possible to change it?

Kind regards,

Hello,

I am trying to run scan-build with crosscheck with z3 like:
scan-build-9 -o scan-report_cc -analyzer-config
'crosscheck-with-z3=true' make

Unfortunately the packages in then official repo here:
https://apt.llvm.org/

are build without Z3 support so I get:
fatal error: error in backend: Clang was not compiled with Z3 support,
rebuild with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON

Is there a reason for this? And is it possible to change it?

The version of z3 in debian is very ancient:
https://tracker.debian.org/pkg/z3 4.4.1-0.4

LLVM needs 4.7 or something.
There is a bug report:
https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=909494

This also affects other LLVM-"affiliated" projects, like alive and souper.

Kind regards,
--
Paulo Matos

Roman.

I think there is a problem with the license as well: Z3 is MIT, so clang would have to be released with Z3’s license.

I _think_ there is a problem with the license as well: Z3 is MIT, so
clang
would have to be released with Z3's license.

I don't think that's a problem. You are not releasing z3 with clang. This is an apt repo. You just need to add the correct dependency on the repo and build using z3 support.

I think there is a problem with the license as well: Z3 is MIT, so
clang
would have to be released with Z3’s license.

I don’t think that’s a problem. You are not releasing z3 with clang. This is an apt repo.

Well, I’m not an expert, but building clang linked with z3 and offering it online for people to download seems a lot like a release.

I don’t it matters if it’s a tar.gz or an apt repo.

Ah, ok you're linking clang with libz3 or so? ...

Still... I am definitely not an expert in licensing but after a quick
lookup on Google, I would say that Apache2 and MIT would not cause a
problem. Anyway, don't quote me on that.

I think there is a problem with the license as well: Z3 is MIT, so
clang
would have to be released with Z3’s license.

I don’t think that’s a problem. You are not releasing z3 with clang.
This is an apt repo.

Well, I’m not an expert, but building clang linked with z3 and offering
it online for people to download seems a lot like a release.

I don’t it matters if it’s a tar.gz or an apt repo.

Ah, ok you’re linking clang with libz3 or so? …

Still… I am definitely not an expert in licensing but after a quick
lookup on Google, I would say that Apache2 and MIT would not cause a
problem. Anyway, don’t quote me on that.

AFAIK, the only requirement is to ship Z3’s license along with the clang.

I heard that there are other projects under the llvm umbrella with the same issue (linking against MIT/apache2 libraries) and that they’re not released with llvm because this requirement.