[cfe-dev] Integration of Z3 for constraint solving [r299463]

[Hans Wennborg via cfe-dev]

Do you want to add something about this in the release notes?

On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
<cfe-dev at lists.llvm.org> wrote:
> This is for the clang static analyzer, when performing symbolic
> execution on input C code. Since the variables are all fixed-width
> bitvectors, and there are no existential/universal quantifiers, in
> practice the performance is decent, although still slower than the
> current range-based constraint manager. However, it allows for reasoning
> over more complex queries, e.g. involving multiple symbolic variables,
> symbolic truncation/extension, and symbolic floating-point expressions
> (these are all follow-up patches that have not yet been merged). There's
> a longer discussion and more concrete performance numbers starting
> around comment https://reviews.llvm.org/D28952#652510 .
>
> Thanks,
>
> Dominic
>
> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>> Hi,
>>
>> I just noticed that Z3 was integrated into the clang frontend to solve
>> some kind of constraints: https://reviews.llvm.org/rL299463
>>
>> What kinds of constraints are these, i.e. which problem are they
>> solving, and is there a possibility of running into an exponential runtime?
>>
>> Kind regards,
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev