Thanks for the topic and the interesting discussion.
I’d like to thank you @DonatNagyE for your time working on this, and I’m looking forward a prototype to test at scale.
Unfortunately, I don’t have much to add to the discussion - maybe only that so far I only considered a relaxed loop-widening invalidation as an option for resolving this.
Lately, I’m also considering some pre-analysis pass on the loop to infer properties of the loops and their variables, such as how a container is being used in a range-based loop (which is more and more common). We could apply the deduced invariants before even entering the loop making it more accurate.
The other side of the coin is that it’s a pity we don’t really find off-by-one errors with the bounds checker, and loop widening or report post processing wouldn’t really change that. I know that’s on the FNs side, and this post is about FPs - yet I still wanted to mention it.
Maybe this one.