[cfe-dev] GSOC | clang Z3

[George Karpenkov via cfe-dev]

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

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