[cfe-commits] r154434 - in /cfe/trunk: include/clang/StaticAnalyzer/Core/PathSensitive/Store.h lib/StaticAnalyzer/Core/ExprEngineC.cpp lib/StaticAnalyzer/Core/RegionStore.cpp test/Analysis/dynamic-cast.cpp

[Jordy Rose]

Nice. There are two PRs about dynamic_cast: PR10380 and PR12366, though neither of them are so encompassing. Does this handle those cases?


On Apr 10, 2012, at 16:59, Anna Zaks wrote:

> +        if (Failed) {
> +          // If the cast fails, conjure symbol constrained to 0.
> +          DefinedOrUnknownSVal NewSym = svalBuilder.getConjuredSymbolVal(NULL,
> +                                 CastE, LCtx, resultType,
> +                                 currentBuilderContext->getCurrentBlockCount());
> +          DefinedOrUnknownSVal Constraint = svalBuilder.evalEQ(state,
> +                                 NewSym, svalBuilder.makeZeroVal(resultType));
> +          state = state->assume(Constraint, true);
> +          state = state->BindExpr(CastE, LCtx, NewSym);

Why is this constrained to 0 instead of just a null? (SValBuilder::makeNull) We don't track anything about null pointers, so we don't need the symbol.


> +        } else {
> +          // If we don't know if the cast succeeded, conjure a new symbol.
> +          if (val.isUnknown()) {
> +            DefinedOrUnknownSVal NewSym = svalBuilder.getConjuredSymbolVal(NULL,
> +                                 CastE, LCtx, resultType,
> +                                 currentBuilderContext->getCurrentBlockCount());
> +            state = state->BindExpr(CastE, LCtx, NewSym);

Since dynamic_casts should /always/ be checked, I feel like we should probably just bifurcate the state here, so that the subexpr value gets propagated. Unfortunately, SValBuilder can't do that...


> +// False negatives.
> +
> +// Symbolic regions are not typed, so we cannot deduce that the cast will
> +// always fail in this case.
> +int testDynCastFail1(class C *c) {
> +  B *b = 0;
> +  b = dynamic_cast<B*>(c);
> +  return b->m;
> +}

Yuck. A syntactic checker would be able to handle this. Why isn't (*c) a TypedRegion on top of the SymbolicRegion?

Also, the class keyword is odd here.

Jordy