[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

steakhal added a comment. In D88019#2303078 , @martong wrote: > I like the second approach, i.e. to have a debug checker. But I don't see, > how would this checker validate all constraints at the moment when they are > added to the State.

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

martong added a comment. In D88019#2296337 , @steakhal wrote: > In D88019#2291953 , @steakhal wrote: > >> What are our options mitigating anything similar happening in the future? >> >> This way any change touching

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

steakhal added a comment. In 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

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

steakhal added a comment. 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,

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rG0c4f91f84b2e: [analyzer][solver] Fix issue with symbol non-equality tracking (authored by martong). Repository: rG LLVM Github Monorepo CHANGES

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

vsavchenko accepted this revision. vsavchenko added a comment. This revision is now accepted and ready to land. Amazing! Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88019/new/ https://reviews.llvm.org/D88019

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

martong updated this revision to Diff 293168. martong marked an inline comment as done. martong added a comment. - Avoid same pattern when checking whether the assumption is infeasible Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88019/new/

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

martong added a comment. Thanks for the quick review! I updated according to your suggestion, so we avoid the same pattern. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1350-1371 ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

vsavchenko added a comment. After this "accepted" and a huge thank you  Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1350-1371 ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt ,

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

vsavchenko added a comment. I came up with exactly the same fix! Great job! I just wanted to refactor it and not having if (New.isEmpty()) // this is infeasible assumption return nullptr; ProgramStateRef NewState = setConstraint(St, Sym, New); return trackNE(NewState, Sym, Int,

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

martong added a comment. @steakhal, thank you for your time and huge effort in debugging this! Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D88019/new/ https://reviews.llvm.org/D88019 ___ cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

martong created this revision. martong added reviewers: vsavchenko, steakhal, NoQ. Herald added subscribers: cfe-commits, ASDenysPetrov, Charusso, gamesh411, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun, whisperity. Herald added a