steakhal added a comment. In D88019#2291953 <https://reviews.llvm.org/D88019#2291953>, @steakhal wrote:
> What are our options mitigating anything similar happening in the future? > > This way any change touching the `SymbolicRangeInferrer` and any related > parts of the analyzer seems to be way too fragile. > Especially, since we might want to add support for comparing SymSyms, just > like we try to do in D77792 <https://reviews.llvm.org/D77792>. What about changing the EXPENSIVE_CHECKS <https://github.com/llvm/llvm-project/blob/d70ec366c91b2a5fc6334e6f6ca9c4d9a6785c5e/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h#L99-L101> in the assume function in the following way: Convert all range constraints into a Z3 model and check if that is `UNSAT`. In that case, we would have returned a state with contradictions, so we would prevent this particular bug from lurking around to bite us later. And another possibility could be to create a debug checker, which registers to the assume callback and does the same conversion and check. This is more appealing to me in some way, like decouples the Z3 dependency from the `ConstraintManager` header. Which approach should I prefer? @NoQ @vsavchenko @martong @xazax.hun @Szelethus Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88019/new/ https://reviews.llvm.org/D88019 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
