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

[Manas Gupta via Phabricator via cfe-commits]

manas 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) {
----------------
vsavchenko wrote:
> 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.
I went through the code and understood that part. I agree that this should be a specialized case for VisitBinaryOperator. So I understand it in this way:

1. Creating a new `VisitBinaryOperator(Range,Range,QualType)` which can check for empty intersections.
2. It will then call to appropriate functions (like `VisittBinaryOperator<BO_NE>` and others.)


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1241
+  // In all other cases, the resulting range cannot be deduced.
+  return RangeFactory.getEmptySet();
+}
----------------
vsavchenko wrote:
> Empty range set means "This situation is IMPOSSIBLE".  Is that what you want here?
True! That's incorrect. We cannot find a good rangeset. Should I rather return the entire RangeSet inferred from `T`?


================
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}}
----------------
vsavchenko wrote:
> Did you try it in debugger, do we get inside of your function?
Yes, the function is being reached.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106102