[cfe-dev] [GSoC Proposal Draft] Integrate z3 SMT solver with Clang Static Analyzer

[George Karpenkov via cfe-dev]

Hi Brenda,

It’s great that you are interested in the project!
However, unfortunately the current proposal is to high-level and does not contain a sufficient level of detail.

I can see the following issues:
 
1) The only example given is on proving DeMorgan’s law, which is unrelated to the proposal
2) It is not specified why or in what cases using an SMT solver would be more precise than using a current solver
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?
“Constructing Z3SolverVisitor”: yes, but what would that visitor do and why?
“Implement z3_solve()”: what constraints? What would this function do?

4) Similar problems appear in the timeline, with evaluation postponed until the very end, and many items being too vague
(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?
Why is the function name relevant at this stage?)

Regards,
George

> On Mar 22, 2018, at 10:18 PM, Brenda So <sogun3 at gmail.com> wrote:
> 
> Hi all,
> 
> 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!
> 
> https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing  <https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing>
> 
> Looking forward to your response,
> Brenda
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180323/d2b12344/attachment.html>