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

[Ted Kremenek via cfe-commits]

krememek added a comment.

In http://reviews.llvm.org/D12358#233983, @zaks.anna wrote:

> A way this could be improved is by invalidating all the values that the loops effects, both the values on the stack and on the heap. (We could even start overly conservative and invalidate all the values in the state; setting the known values to unknown values.)


I worry that this would be far too conservative, and would introduce new false positives because of lost precision.

One unsound hack would be to analyze a loop once by unrolling, and then invalidate anything that was touched in the ProgramState during that loop iteration.  That invalidation could also be transitive, e.g. any subregions of touched state, etc.

Another, more principled hack, would be to look at all DeclRefExprs within a loop and invalidate all memory in the cone-of-influence of those variables (i.e., values they point to, etc.), but that's it.

Then there is the problem of called functions within the loop, as they won't be analyzed.  Those could interfere with the ability of a checker to do its job.

My recommendation is that we still unroll loops a couple times, getting full precision, and then employ a widening technique like the ones being discussed to allow the last loop iteration to act as the last one, but as a conservative over-approximation.


http://reviews.llvm.org/D12358