<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="">It’s great that you are interested in the project!</div><div class="">However, unfortunately the current proposal is to high-level and does not contain a sufficient level of detail.</div><div class=""><br class=""></div><div class="">I can see the following issues:</div><div class=""> </div><div class="">1) The only example given is on proving DeMorgan’s law, which is unrelated to the proposal</div><div class="">2) It is not specified why or in what cases using an SMT solver would be more precise than using a current solver</div><div class="">3) Breaking down into parts is a bit arbitrary: e.g. “Flag bugs in Bug Reporter”: how would you plan to do this? Why a new bug type is needed?</div><div class="">“Constructing Z3SolverVisitor”: yes, but what would that visitor do and why?</div><div class="">“Implement z3_solve()”: what constraints? What would this function do?</div><div class=""><br class=""></div><div class="">4) Similar problems appear in the timeline, with evaluation postponed until the very end, and many items being too vague</div><div class="">(e.g. how would bug reporter figure out which paths are too complex? What “complex” means in this case? What would z3_solve function do?</div><div class="">Why is the function name relevant at this stage?)</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 22, 2018, at 10:18 PM, Brenda So <<a href="mailto:sogun3@gmail.com" class="">sogun3@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class="">Hi all,<br class=""><br class=""></div>Base on the previous discussions on the cfe-dev mailing list and my personal research, I wrote a proposal for integrating z3 SMT solver with clang static analyzer. Base on George's advice, I would like the cfe-dev community to take a look at the proposal and give me some feedback. I do not have much experience with the Clang Static Analyzer so there might be some misunderstanding on my part, therefore any feedback is appreciated!<br class=""><br class=""><a href="https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing" class="">https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing </a><br class=""><br class=""></div><div class="">Looking forward to your response,<br class=""></div>Brenda<br class=""><div class=""><br class=""></div></div>
</div></blockquote></div><br class=""></div></body></html>