[llvm-dev] [cfe-dev] SMT solvers in clang SA

[Siddharth Shankar Swain via llvm-dev]

Thanks Mikhail. Can you tell while refuting false positives does inclusion
of SMT solvers lead to elimination of some genuine issues by mistake ?

On Fri, Sep 21, 2018 at 5:21 PM Mikhail Ramalho <mikhail.ramalho at gmail.com>
wrote:

> We are currently implementing the backends for other solvers (you can
> follow the progress here: https://github.com/mikhailramalho/clang). So
> far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon.
>
> When used to refute bugs, they all give roughly the same results: a ~5%
> speedup if there are refuted bugs or a ~5% slowdown if no bug is refuted.
>
> I've only tried to analyze one full project (tmux) with Yices; the CSA ran
> for 24hrs and it didn't complete the analyze. For comparison, it takes 90s
> to analyze it with the ranged constraint manager in the CSA.
>
> Thanks,
>
> Em sex, 21 de set de 2018 às 12:32, Siddharth Shankar Swain via cfe-dev <
> cfe-dev at lists.llvm.org> escreveu:
>
>> Hi all,
>>
>> Currently studying the impact of SMT solvers on Clang SA. Can anyone help
>> in telling more about the SMT solvers use in clang SA ? ( Have already
>> tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT
>> solvers if possible )
>>
>> Thanks,
>> Siddharth
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>
>
> --
>
> Mikhail Ramalho.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20180921/f02d9bdc/attachment.html>