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

[Parth Thakkar via cfe-dev]

Thanks George! I have a better idea of the project now. I'll get back after
going through the materials you sent as well as more of the code.

Regards
Parth

On Mar 6, 2018 4:16 AM, "George Karpenkov" <ekarpenkov at apple.com> wrote:

> 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 Video “Building a Checker
> in 24 Hours”, slides: 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
>
> 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/20180306/4b72cf05/attachment.html>