[PATCH] D131006: [analyzer] Use DisequalityMap while inferring constraints

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

In D131006#3699017 <https://reviews.llvm.org/D131006#3699017>, @martong wrote:

> Awesome!

Thank you!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1512-1516
+        if (IsFirst) {
+          IsFirst = false;
+          RS = *RSPtr;
+        } else
+          RS = RangeFactory.unite(RS, *RSPtr);
----------------
martong wrote:
> `unite` should be working with an empty set as well, shouldn't it?
You are right.

It's interesting that for some reason I was sure that `unite` returns //empty// if any given set is //empty// (mixed up with `intersect`). And this is at a time when I'm the author of `unite` :-P


================
Comment at: clang/test/Analysis/range-inferring-from-disequality-map.cpp:50-51
+    if(x != tmp1 && x != tmp2)
+      // TODO: This condition should be infeasible.
+      //       Thus, the branch should be unreachable.
+      clang_analyzer_value(x); // expected-warning {{{ empty }}}
----------------
martong wrote:
> Why can't we return an empty set from `getInvertedRangeFromDisequalityMap` in this case? `intersect` should handle the rest then.
Currently, we can't.  At least, in this patch.
We produce infeasible branches (aka `nullptr` `ProgramStateRef`) when use `ConstraintAssignor::assign`.
But here we use `SymbolicRangeInferrer` which only produces a RangeSet. In other words, we don't store this range anywhere but infer it every time.

Basically, this is a work for the next patches. They should remove the TODOs.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D131006