<div dir="ltr"><div dir="ltr">It's possible and it happened before (see: <a href="https://reviews.llvm.org/D48324">https://reviews.llvm.org/D48324</a>), but I haven't seen any true positive being removed lately.</div></div><br><div class="gmail_quote"><div dir="ltr">Em sex, 21 de set de 2018 às 13:03, Siddharth Shankar Swain <<a href="mailto:h2015096@pilani.bits-pilani.ac.in">h2015096@pilani.bits-pilani.ac.in</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks Mikhail. Can you tell while refuting false positives does inclusion of SMT solvers lead to elimination of some genuine issues by mistake ?</div><br><div class="gmail_quote"><div dir="ltr">On Fri, Sep 21, 2018 at 5:21 PM Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr">We are currently implementing the backends for other solvers (you can follow the progress here: <a href="https://github.com/mikhailramalho/clang" target="_blank">https://github.com/mikhailramalho/clang</a>). So far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon.</div><div dir="ltr"><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Thanks, </div></div><br><div class="gmail_quote"><div dir="ltr">Em sex, 21 de set de 2018 às 12:32, Siddharth Shankar Swain via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>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 )</div><div><br></div><div>Thanks,</div><div>Siddharth</div></div>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="m_226953090311171419m_3924583509847514868gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</blockquote></div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>