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

[Mikhail Ramalho via cfe-commits]

>
>
> Awesome! Does it mean that the optimization for adding less constraints
> was in fact buggy?
>
>
I pretty sure it was not related to the optimizations, I removed them days
ago (in the previous version of this patch) and the bug was still there.


>
> 2. Could it be something unrelated to your changes? Any given trunk
> version can be buggy, but usually those are resolved very fast, so if you
> update now the issue can go away.
>
> Watching cfe-commits mailing list might be helpful there.
>
>
I update my repo every other day and it's been happening for the past
two/three weeks :/

The compiler shows the following error:

posix_spawn failed: Argument list too long

There are some discussions in several places about it.

-- 

Mikhail Ramalho.
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Re: [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.
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits