[cfe-dev] Need sources to read up about Z3 integration GSOC project

[George Karpenkov via cfe-dev]

Hi Parth,

> 
> Besides these two I could not find any material relevant to this project. It would be great if someone could point out additional reading material relevant to this.

Yes, unfortunately getting into the analyzer development is rather hard.
Two good entry points are:

 - https://www.youtube.com/watch?v=kdxlsP5QVPw <https://www.youtube.com/watch?v=kdxlsP5QVPw> Video “Building a Checker in 24 Hours”, slides: http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf <http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf>
 - Additionally, Artem has written a very good guide available at https://github.com/haoNoQ/clang-analyzer-guide <https://github.com/haoNoQ/clang-analyzer-guide> 

> Since there has already been a merged item of integrating Z3, I'd like to know what the expected outcomes of this project would be.

The project you have linked to had a goal of replacing the analyzer constraint manager with Z3.
The evaluation has shown a massive (> 20x) slowdown.

The motivation for the current project is that false positives is, perhaps, the largest problem static analyzer has
(that is, bug reports where the analyzer reports a bug due to imprecision, but no bug actually exists).
Thus, the idea is to analyze the project with the currently used fast and imprecise solver,
but then try to refute bug reports in the post-processing phase using the Z3 solver.

> 
> Regards
> Parth
> 
> 
> 
> ‌
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

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