https://github.com/NagyDonat approved this pull request.
This commit looks good at first glance, and given that `SMTConstraintManager` is an unsupported prototype (that crashes on any large codebase), I give an approval – assuming that you ( @rdevshp ) verified the correctness of this change. I have some minor nitpicks in inline comments, have a look at them, but the change is OK even if you ignore them. Also, please wait a few days in case @steakhal has time to add something (he knows a bit more than me about this part of the analyzer). ------- Your motivation for this patch is very clear: the core advantage of using `Z3` as the constraint manager is that it is capable of complex reasoning, and we throw out this one advantage if the "dead" symbol removal is too aggressive. (Even with the less smart range-based constraint manager we sometimes run into situations where we lose information that would be useful.) However, note that symbol liveness is used for many things, so this extended lifetime may cause surprising side effects. For example, memory leak warnings are reported when the pointer to the allocated area becomes dead -- but this would keep the pointer symbol alive if e.g. the result of a comparison operator is still alive. For this reason, I'm not completely sure if this is the theoretically correct approach, but from a practical POV I don't see any serious threat. https://github.com/llvm/llvm-project/pull/215240 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
