[cfe-dev] GSOC | clang Z3

[Ashish Gahlot via cfe-dev]

Hello all,

I will be submitting my proposal within a couple of days for the community
review. Please add your valuable comments so that I can refactor the
proposal.
I have never worked with solvers before so it is pretty new for me. I am
not able to figure out the exact reason for the slowing down of the solver
and the reason it generates false positives by just reading the code. Can
you please give me some pointers where should I focus on?

Thank you very much,
Ashish Kumar Gahlot

On Fri, Mar 16, 2018 at 11:06 PM, George Karpenkov <ekarpenkov at apple.com>
wrote:

> Hi Ashish,
>
> On Mar 15, 2018, at 11:41 PM, Ashish Gahlot via cfe-dev <
> cfe-dev at lists.llvm.org> wrote:
>
> Hello all,
>
> I was testing the performance of the z3 clang analyzer using the
> sv-benchmarks
> <https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-industry-pattern/ofuf_1_true-unreach-call.c>.
> I experienced a huge performance issue in the analyzer[image
> <https://imgur.com/a/rEa1X>].
>
>
> Yes, hence the point of the GSOC project to only cross-check the
> counterexamples.
>
> Is there a way we can use something similar to *z3 -v<N> *when we run the
> analyzer to see where the z3 is getting stuck?
>
>
> No, there is no similar option for the analyzer.
> I don’t think it would help you much though: most likely z3 is just
> performing a very large number of small queries at every step.
>
>
> Another thing I wanted to ask is that does LLVM has a particular format in
> which a student has to submit his proposal?
>
>
> Probably the easiest is to search the list archives from the last year and
> to look for the previous analyzer GSoC applications.
>
> Regards,
> George
>
>
> Thank You,
> Ashish Kumar Gahlot
>
> --
> Ashish Kumar Gahlot
> IV year, UG
> Govt. Engg. College, Ajmer, India
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
>


-- 
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180322/f7c3d411/attachment.html>