ymandel added inline comments.
================
Comment at:
clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp:279
+ cast_or_null<BoolValue>(Env.getValue(*ComparisonExprLoc))) {
+ Env.setValue(*ComparisonExprLoc,
+ Env.makeAnd(*CurrentValue, ComparisonValue));
----------------
xazax.hun wrote:
> I am still wondering a bit about this case.
>
> We generate: `HasValueVal and ContentsNotEqX and CurrentValue`.'
> I wonder if we want: `HasValueVal and (ContentsNotEqX <=> CurrentValue)`
> instead? Or even `HasValueVal and CurrentValue`?
I don't think that the iff version is right, but `HasValueVal and
CurrentValue` could be. My concern is that we're not guaranteed that
`CurrentValue` is populated. And, even if we were, it doesn't feel quite right.
Assuming its a high fidelity model, we get (logically): `HasValue(opt) and
Ne(ValueOr(opt,X),X)`. Then, when negated (say, on an else branch) we get
`not(HasValue(opt)) or not(Ne(ValueOr(opt,X),X))` which is equivalent to
`not(HasValue(opt)) or Eq(ValueOr(opt,X),X)`. While true, it seems redundant,
since the first clause should be derivable from the second (assuming an
interpretatable semantics to the `ValueOr` predicate).
Regardless, it might be better to step back and figure out how this should be
done systematically. I'll try to come back with a proposal on that.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D122231/new/
https://reviews.llvm.org/D122231
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
