[PATCH] D30489: [analyzer] catch out of bounds for VLA

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In https://reviews.llvm.org/D30489#728945, @danielmarjamaki wrote:

> I would propose that I rename and cleanup RangeConstraintManager::uglyEval() and add it. When I tested it, the Z3 does not seem to handle this.


What do you mean by Z3 not handling this? I mean, if the evalEq returns an unknown SVal, Z3 can not do anything with that. Does Z3 fails after the evalEq returns the correct SVal?

I wonder that is the reason that we do not produce the correct SVal right now. Maybe the reason was that, we do not want to produce SVals that the constraint manager can not solve anyways, to improve performance. In general the current constraint manager does not reason about SymSymExprs. In order to preserve the performance we might not want to start produce all kinds of SymSymExprs, only the cases we already handle in the constraint managers.

E.g.: it might make sense to produce something like ` $a - $b =0`, so https://reviews.llvm.org/rL300178 can kick in, and in some cases we might be able to find the bug (e.g. the function in the example was called with a concrete int).


Repository:
  rL LLVM

https://reviews.llvm.org/D30489