<div dir="auto">Thanks George! I have a better idea of the project now. I'll get back after going through the materials you sent as well as more of the code.<div dir="auto"><br></div><div dir="auto">Regards</div><div dir="auto">Parth</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mar 6, 2018 4:16 AM, "George Karpenkov" <<a href="mailto:ekarpenkov@apple.com">ekarpenkov@apple.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Hi Parth,<div><br></div><div><div><blockquote type="cite"><div><div dir="ltr"><div><br></div><div>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></div>Yes, unfortunately getting into the analyzer development is rather hard.</div><div>Two good entry points are:</div><div><br></div><div> - <a href="https://www.youtube.com/watch?v=kdxlsP5QVPw" target="_blank">https://www.youtube.com/<wbr>watch?v=kdxlsP5QVPw</a> Video “Building a Checker in 24 Hours”, slides: <a href="http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf" target="_blank">http://llvm.org/<wbr>devmtg/2012-11/Zaks-Rose-<wbr>Checker24Hours.pdf</a></div><div> - Additionally, Artem has written a very good guide available at <a href="https://github.com/haoNoQ/clang-analyzer-guide" target="_blank">https://github.com/haoNoQ/<wbr>clang-analyzer-guide</a> <br><br><blockquote type="cite"><div><div dir="ltr"><div>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></div></div></div></blockquote><div><br></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></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><blockquote type="cite"><div><div dir="ltr"><div><br></div><div>Regards</div><div>Parth<br></div><div><br><br><br>‌</div></div>
______________________________<wbr>_________________<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" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br></div></blockquote></div><br></div></div></blockquote></div></div>