clang in official apt repo built without z3 support

classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev
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,
--
Paulo Matos
_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev
On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
<[hidden email]> wrote:

>
> 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.

> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev
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. 

On Tue, 12 Feb 2019, 09:24 Roman Lebedev via cfe-dev <[hidden email] wrote:
On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
<[hidden email]> wrote:
>
> 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.

> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev


On 12 February 2019 18:59:21 CET, Mikhail Ramalho <[hidden email]> wrote:
>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.

>
>On Tue, 12 Feb 2019, 09:24 Roman Lebedev via cfe-dev
><[hidden email]
>wrote:
>
>> On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
>> <[hidden email]> wrote:
>> >
>> > 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.
>>
>> > _______________________________________________
>> > cfe-dev mailing list
>> > [hidden email]
>> > https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>> _______________________________________________
>> cfe-dev mailing list
>> [hidden email]
>> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>

--
Paulo Matos
_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev


On Tue, 12 Feb 2019, 14:32 Paulo Matos <[hidden email] wrote:


On 12 February 2019 18:59:21 CET, Mikhail Ramalho <[hidden email]> wrote:
>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.

You just need to add the correct dependency on the repo and build using  z3 support.

>
>On Tue, 12 Feb 2019, 09:24 Roman Lebedev via cfe-dev
><[hidden email]
>wrote:
>
>> On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
>> <[hidden email]> wrote:
>> >
>> > 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.
>>
>> > _______________________________________________
>> > cfe-dev mailing list
>> > [hidden email]
>> > https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>> _______________________________________________
>> cfe-dev mailing list
>> [hidden email]
>> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>

--
Paulo Matos

_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev


On 12/02/2019 19:49, Mikhail Ramalho wrote:

>
>
> On Tue, 12 Feb 2019, 14:32 Paulo Matos <[hidden email] wrote:
>
>
>
>     On 12 February 2019 18:59:21 CET, Mikhail Ramalho
>     <[hidden email] <mailto:[hidden email]>> wrote:
>     >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.

--
Paulo Matos
_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: clang in official apt repo built without z3 support

Ilya Biryukov via cfe-dev


On Tue, 12 Feb 2019, 15:57 Paulo Matos <[hidden email] wrote:


On 12/02/2019 19:49, Mikhail Ramalho wrote:
>
>
> On Tue, 12 Feb 2019, 14:32 Paulo Matos <[hidden email] wrote:
>
>
>
>     On 12 February 2019 18:59:21 CET, Mikhail Ramalho
>     <[hidden email] <mailto:[hidden email]>> wrote:
>     >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. 



--
Paulo Matos

_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev