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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

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

> Do you agree that this is the problem? Would it be a good idea to try to keep the sz in the ProgramState?


Environment stores values only temporarily. It's kind of a scratch pad for temporary symbolic calculations: we compute sub-expressions, put them in the Environment, compute the expression itself, then throw the sub-expressions away immediately. Store, on the other hand, is a permanent storage.

Also, in your state dumps no information is actually lost. The fact that the value of variable `sz` is `reg_$0<sz>` is trivial: you could ask the Store what's the value of the variable `sz` and it'd say `reg_$0<sz>` if there are no bindings over it.

Or, alternatively, you see the same value in the dump of the ElementRegion as its index.

P.S. I'd agree that it's better to merge the two versions of the checker than trying to fix one of them to be at least as good as the other, through different approaches.


Repository:
  rL LLVM

https://reviews.llvm.org/D30489