[PATCH] D106102: [analyzer][solver] Introduce reasoning for not equal to operator

Sat Oct 23 15:34:00 PDT 2021

manas added a comment.

Based on the information from debugger, the logs <https://reviews.llvm.org/F19816216$339-341> show RangeSets `[0, 255]` and `[INT_MIN, 0]` from different types <https://reviews.llvm.org/F19816216$352-359> are causing the failure.
I tried producing a compact test case <https://reviews.llvm.org/F19816126>. The essential part is the comparison between different types, as in this case `unsigned int` and `int`. In other binary operators (BO_And, BO_Rem, etc.), this gets handled by coarsing RangeSets to Ranges and converting those Ranges to resulting type for comparison. This is missing in `BO_NE`. I suppose, this may be the reason behind the signedness mismatch.

One way to solve this would be to let the specialization of `VisitBinaryOperator` (definition here <https://github.com/llvm/llvm-project/blob/main/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp#L998>) handle the coarse/convert, and then `VisitBinaryOperator<BO_NE>` checking for any reasonable result which can be inferred from those Ranges.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106102