[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via cfe-commits]

Hi,


> Just a bit of context and to have some expectation management regarding
> this patch. The main purpose of this implementation was to back a thesis.
> It was made under a very serious time pressure and the main goal was to be
> able to measure on real world projects as soon as possible and in the
> meantime to be flexible so we can measure multiple configurations (like
> incremental solving).
>
> So the goal was a flexible proof of concept that is sensible to measure in
> the shortest possible time. After the thesis was done, Reka started to work
> an another GSoC project, so she had no time to review the code with the
> requirements of upstreaming in mind. Nevertheless we found that sharing the
> proof of concept could be useful for the community.  So it is perfectly
> reasonable if you disagree with some design decisions behind this patch,
> because the requirements for the thesis (in the short time frame) was very
> different from the requirements of upstreaming this work. In a different
> context these decisions made perfect sense.
>
>
Just want to comment here and give thanks again for the first version of
the refutation code. It's being really helpful to develop the approach this
code as a base; things would definitely be slower if I had to start it from
scratch.

Thanks!

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180531/0666a155/attachment.html>