================
@@ -1224,16 +1224,33 @@ void ExprEngine::VisitLambdaExpr(const LambdaExpr *LE,
ExplodedNode *Pred,
void ExprEngine::VisitAttributedStmt(const AttributedStmt *A,
ExplodedNode *Pred, ExplodedNodeSet &Dst)
{
+ const LocationContext *LCtx = Pred->getLocationContext();
ExplodedNodeSet CheckerPreStmt;
getCheckerManager().runCheckersForPreStmt(CheckerPreStmt, Pred, A, *this);
ExplodedNodeSet EvalSet;
- NodeBuilder Bldr(CheckerPreStmt, EvalSet, *currBldrCtx);
- for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
- for (ExplodedNode *N : CheckerPreStmt) {
- Visit(Attr->getAssumption()->IgnoreParens(), N, EvalSet);
+ for (ExplodedNode *N : CheckerPreStmt) {
+ ProgramStateRef State = N->getState();
+ for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
+ SVal AssumedVal = State->getSVal(Attr->getAssumption(), LCtx);
+ if (auto ValidAssumedVal = AssumedVal.getAs<DefinedOrUnknownSVal>()) {
+ State = State->assume(*ValidAssumedVal, true);
+ } else {
+ // The assumption expression has evaluated to UndefinedVal.
----------------
NagyDonat wrote:
> Traditionally, just because something produced undef, we usually don't
> terminate the exploration.
You are right that _producing_ an undefined (not just unknown) value is not
always reported (e.g. the contents of the buffer returned by `malloc` are undef
and this is fine), although even there we have
`core.UndefinedBinaryOperatorResult` which reports situations when a binary
operator produces undef.
On the other hand, all the reasonably common ways of _using_ undef are all
reported by various `core` checkers:
- assigning undef to a variable is reported by `core.uninitialized.Assign`,
- using undef in the condition of a control flow statement is reported by
`core.uninitialized.Branch`,
- passing undef to a function is reported by `core.CallAndMessage`, ...
> What is the rationale here?
I think using a value in `[[assume(...)]]`` is analogous to passing it to a
function or using it in the condition of an `if`, so the analyzer should behave
analogously, i.e. sink the execution path. This would be consistent with the
behavior of an `assert(...)` call.
Also, I think it would be very rare to `[[assume(...)]]` expressions that are
really undefined, so is suspect that a significant fraction of the (rare)
`UndefinedVal`s encountered at this point would be produced by bugs in the
analyzer engine. (And in that case discarding the inconsistent state is the
right thing to do.)
However I can also accept "just ignore the undefined assumption" if you
strongly prefer that.
https://github.com/llvm/llvm-project/pull/198618
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
