martong added inline comments.
================
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 }}}
----------------
ASDenysPetrov wrote:
> 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.
You mean this hunk?
```
for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange(
RangeFactory, State, DisequalClass);
UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point);
// If we end up with at least one of the disequal classes to be
// constrained with an empty range-set, the state is infeasible.
if (UpdatedConstraint.isEmpty())
return nullptr;
```
Yeah, I am not sure why do we infer a range here instead of simply getting the
associated range from the constraint set. Inferring here might result with an
inconsistent result. I think we should infer only in the
`SymbolicRangeInferrer`.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D131006/new/
https://reviews.llvm.org/D131006
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
