<div dir="ltr"><div><div>Hi George,<br><br></div>Thanks for the advice! I found a bug on Bugzilla that addresses exactly what I want to do in this project -- using Z3 to track symbolic values in the program since the current analyzer doesn't have the power to do so. I believe this could be a beneficial add on to the clang static analyzer! I addressed issues 1 and 2 by adding a motivational example and demonstrated how z3 can be used to solve the problem.<br><br></div><div>I also added a lot more detail under ProjectGoal and Implementation -- hopefully that addressed issues 3 and 4. In the timeline I laid out plans to test each step of the program. <br></div><div><br></div>Moreover, I realize that modifying the BugReporter internally might be too difficult, so I put it as an extra goal instead. <br><div><br></div><div>I  updated the proposal with the above changes. Again if you have any concerns please let me know!<br><a href="https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing"><br>https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing </a><br><br></div><div>Yours,<br></div><div>Brenda<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 23, 2018 at 1:53 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 Brenda,<div><br></div><div>It’s great that you are interested in the project!</div><div>However, unfortunately the current proposal is to high-level and does not contain a sufficient level of detail.</div><div><br></div><div>I can see the following issues:</div><div> </div><div>1) The only example given is on proving DeMorgan’s law, which is unrelated to the proposal</div><div>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>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>“Constructing Z3SolverVisitor”: yes, but what would that visitor do and why?</div><div>“Implement z3_solve()”: what constraints? What would this function do?</div><div><br></div><div>4) Similar problems appear in the timeline, with evaluation postponed until the very end, and many items being too vague</div><div>(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>Why is the function name relevant at this stage?)</div><div><br></div><div>Regards,</div><div>George</div><div><div class="h5"><div><div><br><blockquote type="cite"><div>On Mar 22, 2018, at 10:18 PM, Brenda So <<a href="mailto:sogun3@gmail.com" target="_blank">sogun3@gmail.com</a>> wrote:</div><br class="m_3142945492896380701Apple-interchange-newline"><div><div dir="ltr"><div><div>Hi all,<br><br></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><br><a href="https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing" target="_blank">https://docs.google.com/<wbr>document/d/1vg1-<wbr>y1P9lChTyZ5ritxC6He-<wbr>jIS8ARSfSryT4nXLhe0/edit?usp=<wbr>sharing </a><br><br></div><div>Looking forward to your response,<br></div>Brenda<br><div><br></div></div>
</div></blockquote></div><br></div></div></div></div></blockquote></div><br></div>