<div dir="ltr"><div><div><div><div>Hello all,<br><br></div>I will be submitting my proposal within a couple of days for the community review. Please add your valuable comments so that I can refactor the proposal.<br></div>I have never worked with solvers before so it is pretty new for me. I am not able to figure out the exact reason for the slowing down of the solver and the reason it generates false positives by just reading the code. Can you please give me some pointers where should I focus on?<br><br></div>Thank you very much,<br></div>Ashish Kumar Gahlot<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 16, 2018 at 11:06 PM, George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span> wrote:<br><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 Ashish,<br><div><span class=""><br><blockquote type="cite"><div>On Mar 15, 2018, at 11:41 PM, Ashish Gahlot via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="m_-4430726470022118834Apple-interchange-newline"><div><div dir="ltr"><div><div><div><div>Hello all,<br><br></div>I was testing the performance of the z3 clang analyzer using the <a href="https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-industry-pattern/ofuf_1_true-unreach-call.c" target="_blank">sv-benchmarks</a>. I experienced a huge performance issue in the analyzer[<a href="https://imgur.com/a/rEa1X" target="_blank">image</a>].</div></div></div></div></div></blockquote><div><br></div></span><div>Yes, hence the point of the GSOC project to only cross-check the counterexamples.</div><span class=""><br><blockquote type="cite"><div><div dir="ltr"><div><div><div> Is there a way we can use something similar to <i>z3 -v<N> </i>when we run the analyzer to see where the z3 is getting stuck?<br></div></div></div></div></div></blockquote><div><br></div></span><div>No, there is no similar option for the analyzer.</div><div>I don’t think it would help you much though: most likely z3 is just performing a very large number of small queries at every step.</div><span class=""><br><blockquote type="cite"><div><div dir="ltr"><div><div><div><br></div>Another thing I wanted to ask is that does LLVM has a particular format in which a student has to submit his proposal?<br></div></div></div></div></blockquote><div><br></div></span><div>Probably the easiest is to search the list archives from the last year and to look for the previous analyzer GSoC applications.</div><div><br></div><div>Regards,</div><div>George</div><br><blockquote type="cite"><div><span class=""><div dir="ltr"><div><div><br></div>Thank You,<br></div>Ashish Kumar Gahlot <br clear="all"><div><div><div><div><div><div><div><br>-- <br><div class="m_-4430726470022118834gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Ashish Kumar Gahlot</div><div>IV year, UG</div><div>Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div></div></div></div></div></div></div></div></span>
______________________________<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></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Ashish Kumar Gahlot</div><div>IV year, UG</div><div>Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div>