martong added a comment.
In D111642#3059467 <https://reviews.llvm.org/D111642#3059467>, @steakhal wrote:
> The coverage report of the test shows that L2124 is uncovered. Please add a
> test demonstrating that path as well.
I've added such a test, thanks for the notice!
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2126-2130
+ // Initiate the reorganization of the equality information. E.g., if we
+ // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+ // sense to do this only with `SymIntExpr`s.
+ // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+ // them.
----------------
steakhal wrote:
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`? If it can
> happen, then we could see such instances and we should do the right thing
> with them as well.
> WDYT?
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`?
Yes it can. However, in order to handle them we should extend
`computeAdjustment` properly, which is absolutely not trivial - considering the
test cases in `additive-folding.cpp` - So, I'd rather address that in another
patch.
================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:36
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+ if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1]
+ return;
----------------
steakhal wrote:
> Please express that `C: [-2,-1]` is then intersected with the already
> associated range which is `[-1,1]`, thus we get `c: [-1,-1]`.
Ok, I've added that comment.
================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:55
+ if (b != 1) // b == 1 --> c + 1 == 0 --> c == -1 contradiction
+ return;
+ clang_analyzer_warnIfReached(); // no warning
----------------
steakhal wrote:
> Can we infer within this true branch that `b` must be `0` to make this path
> feasible?
> If we already can infer this, can we put there the appropriate assertion?
> If not, an assertion would be justified with a FIXME.
> Can we infer within this true branch that `b` must be `0` to make this path
> feasible?
Yes, we can.
> If we already can infer this, can we put there the appropriate assertion?
Ok, I've added the appropriate `clang_analyzer_eval` to check this.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D111642/new/
https://reviews.llvm.org/D111642
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
