NoQ added a comment.
An idea. I believe the safest way to find the bugs you mentioned would be to
replace extent-as-a-symbol with extent-as-a-trait.
I.e., currently we construct `extent_$3{SymRegion{conj_$1{char *}}}`, assume
that it is equal to `reg_$0<int X>` (which produces a `SymSymExpr`) and then
catch more `SymSymExpr`s along the path and compare them to the first one.
Instead, i believe that from the start we should have done something like
REGISTER_MAP_WITH_PROGRAMSTATE(RegionExtent, const SubRegion *, NonLoc);
Then when the VLA is constructed (or memory is malloc'ed or something like
that), we just set the `RegionExtent` trait directly to `reg_$0<int X>` and
later easily compare it to anything. The region's `getExtent()` method would be
modified to consult this trait instead of (or, at least, before) constructing a
new symbol.
Ideologically it is the same thing. Technically it produces simpler symbolic
expressions, and i believe that both RangeConstraintManager and Z3 would
benefit from simpler symbolic expressions.
Repository:
rL LLVM
https://reviews.llvm.org/D30489
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
