<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 Brenda,<div class=""><br class=""></div><div class="">Great that you are interested in the project! </div><div class="">I’m reposting this to cfe-dev as Clang development is discussed there (please direct all future email to that list).</div><div class=""><br class=""></div><div class="">As to your question, I think I have answered it in the following email: <a href="http://lists.llvm.org/pipermail/cfe-dev/2018-March/057067.html" class="">http://lists.llvm.org/pipermail/cfe-dev/2018-March/057067.html</a></div><div class="">(yes, lack of easily searchable/browsable archives is a problem..)</div><div class=""><br class=""></div><div class="">Regards,</div><div class="">George</div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 14, 2018, at 6:37 PM, Brenda So via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" class="">llvm-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi all,</div><div class=""><br class=""></div><div class="">I am a fourth year EE bachelors student who is very interested in compilers. I have taken the only compilers course offered in my school and did an independent study with my CS professor. Although I'll begin to work in a couple of months, I definitely want to pursue my interest in compiler design and optimization as a PhD in the future. I am very interested in the z3 SMT solver project detailed on the LLVM website and have been doing some research about it. </div><div class=""><br class=""></div>From what I understand, the current analyzer <font face="arial, helvetica, sans-serif" class=""><span style="line-height: 107%;" class="">traces the program, and at each branch, it branches out into the true
branch and the false branch. The true and false branch causes certain
constraints on the values. If the conditions on the branch causes a constraint
to be unsatisfiable, the path is considered to be infeasible. </span>
<span style="line-height: 107%;" class="">traces the program, and at each branch, it branches out into the true
branch and the false branch. The true and false branch causes certain
constraints on the values. If the conditions on the branch causes a constraint
to be unsatisfiable, the path is considered to be infeasible. In that case, z3 would be useful in proving whether a branch is definitely true or false (i.e. whether the constraints are satisfiable), thus preventing exponential blowup of the analysis. </span></font><div class=""><br class=""></div><div class="">However, when I was looking through the github version of LLVM, it seems like z3 is already incorporated: </div><div class=""><a href="https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp" class="">https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp</a> <br class=""></div><div class=""><br class=""></div><div class="">I guess my question is, what would the project contribute on top of the z3 manager that is currently implemented for LLVM?</div><div class=""><br class=""></div><div class="">Thanks!</div><div class="">Brenda</div></div>
_______________________________________________<br class="">LLVM Developers mailing list<br class=""><a href="mailto:llvm-dev@lists.llvm.org" class="">llvm-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev<br class=""></div></blockquote></div><br class=""></div></body></html>