https://github.com/steakhal commented:
Thank you for the ping. I'm really busy lately with stabilizing Z3 refutation.
I really liked the extensive evaluation, which helped a lot forming my opinion
here.
The diffs look all right. I only spotchecked some places the reports. I agree
with your evaluation.
The content of the patch looks also correct. I only found a couple Grammarly
spellings, but that's it.
I wonder how you found out that loop widening may conflict with this heuristic,
were any tests broken that raised your awareness?
I have one concern with `didEagerlyAssumeBifurcateAt`, that it is bound and
overwritten at the most recent eager split - which to my knowledge may not be
the loop condition if we have something like this:
```c++
while (coin()) {
if (coin()) { // #inner_coin
++num;
}
}
```
Each time the `inner_coin` would spoil the `LastEagerlyAssumeBifurcationAt`
trait between the loop iterations, right?
Storing `const Expr *` pointers is brittle for recursive functions too, where
the same expression could appear in different LocationContexts. I wonder if we
could make an example where it would confuse this heuristic.
I'm also not entirely convinced about nested loops - if this heuristic would
kick in. This is basically a variant of the `coin` case I showed an example.
I don't have a counter example just yet, but I'm not sure I can spare the time
to craft one.
Once again, big kudos for the extensive data. And I have no objections overall,
I only have these minor questions before I'd approve this.
https://github.com/llvm/llvm-project/pull/119388
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
