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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1223-1225
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(Range LHS, Range RHS,
+                                                           QualType T) {
----------------
I think it should be a specialization for another `VisitBinaryOperator`.
In the switch, you can see that we give range sets for `LHS` and `RHS`, so how does it work?
There is a function in between (also `VisitBinaryOperator`) that creates simple ranges out of range sets and ask to visit binary operator for those.  You can specialize it instead since we can simply check for empty intersection of range sets.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1241
+  // In all other cases, the resulting range cannot be deduced.
+  return RangeFactory.getEmptySet();
+}
----------------
Empty range set means "This situation is IMPOSSIBLE".  Is that what you want here?


================
Comment at: clang/test/Analysis/constant-folding.c:470-504
+  // Checks when ranges are not overlapping
+  if (a <= 10 && b >= 20) {
+    clang_analyzer_eval((a != b) != 0); // expected-warning{{TRUE}}
+  }
+
+  if (c <= INT_MIN + 10 && d >= INT_MAX - 10) {
+    clang_analyzer_eval((c != d) == 0); // expected-warning{{FALSE}}
----------------
Did you try it in debugger, do we get inside of your function?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106102