[PATCH] D75698: [analyzer][WIP] Suppress bug reports where a tracked expression's latest value change was a result of an invalidation

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

> P.S. So, like, we could try to emit the warning only if we covered enough execution paths to prove that there's either dead code or the warning is true. Then we would no longer care about invalidation problems. Unfortunately, i don't have any specific suggestion of how to prove such facts for an arbitrary CFG.

If I understand you correctly, this would mean that we have to reason about all possible execution paths at the same time to do this. Actually, that would be possible only with some kind of a fix-point flow-analysis and clearly the symbolic execution we have in CSA is a completely different beast (it reasons about one path where there is a bug).

> P.P.S. Actually you know what, maybe we should only drop the report if the constraint over the invalidated value contradicts the constraint over the old value. That'll make things a bit more complicated and will require a visitor indeed, though hopefully not as complicated as concrete value tracking, as we're still interested in only one region at a time.

How would that be different than proving the feasibility of the path with Z3? Could we reuse Mikhail's work here, or that would be overkill for this task?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D75698/new/

https://reviews.llvm.org/D75698