<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Parth,<div class=""><br class=""></div><div class=""><div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Besides these two I could not find any material relevant to this project. It would be great if someone could point out additional reading material relevant to this. </div></div></div></blockquote><div><br class=""></div>Yes, unfortunately getting into the analyzer development is rather hard.</div><div>Two good entry points are:</div><div><br class=""></div><div> - <a href="https://www.youtube.com/watch?v=kdxlsP5QVPw" class="">https://www.youtube.com/watch?v=kdxlsP5QVPw</a> Video “Building a Checker in 24 Hours”, slides: <a href="http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf" class="">http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf</a></div><div> - Additionally, Artem has written a very good guide available at <a href="https://github.com/haoNoQ/clang-analyzer-guide" class="">https://github.com/haoNoQ/clang-analyzer-guide</a> <br class=""><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">Since there has already been a merged item of integrating Z3, I'd like to know what the expected outcomes of this project would be.<br class=""></div></div></div></blockquote><div><br class=""></div><div>The project you have linked to had a goal of replacing the analyzer constraint manager with Z3.</div><div>The evaluation has shown a massive (> 20x) slowdown.</div><div><br class=""></div><div>The motivation for the current project is that false positives is, perhaps, the largest problem static analyzer has</div><div>(that is, bug reports where the analyzer reports a bug due to imprecision, but no bug actually exists).</div><div>Thus, the idea is to analyze the project with the currently used fast and imprecise solver,</div><div>but then try to refute bug reports in the post-processing phase using the Z3 solver.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Regards</div><div class="">Parth<br class=""></div><div class=""><br class=""><br class=""><br class=""></div></div>
_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></div></blockquote></div><br class=""></div></body></html>