[PATCH] D12358: [Analyzer] Handling constant bound loops

[Devin Coughlin via cfe-commits]

dcoughlin added a comment.

Sean,

One important difference between what you are proposing and what Cousot and Cousot describe in the paper you cite is that they don't drop coverage. They widen for termination on infinite-height lattices and their narrowing still maintains an over-approximation (it covers all potential paths through a loop -- and perhaps some extra ones as well). What the analyzer had before with constant-bound loops was an under-approximation: it would just stop exploring paths after a while

What you are proposing is neither an under-approximation nor an over-approximation because it will both drop coverage (e.g., the path in my simple example above where `i` is 21 after the loop) and add spurious paths (e.g., the path where `i` is 23). This is something that it is best to avoid when possible because it will cause the analyzer to both miss true positives and lead to false positives.


http://reviews.llvm.org/D12358