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

[Mikhail Ramalho via llvm-dev]

It's possible and it happened before (see: https://reviews.llvm.org/D48324),
but I haven't seen any true positive being removed lately.

Em sex, 21 de set de 2018 às 13:03, Siddharth Shankar Swain <
h2015096 at pilani.bits-pilani.ac.in> escreveu:

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

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20180921/d914c8ea/attachment.html>