necto wrote: > But even in C, the condition expression of `if` should be resolved as `cond > == 0` and `cond != 0` for the two states, right? That is effectively the same > as the implicit bool conversion in C++.
No. In C the condition does not get implicitly substituted by `cond != 0`. The engine assuems `cond == 0` and `cond != 0`, but it does not simplify `cond` when doing so. If I write the condition `if (... != 0)` the infeasible path is no longer taken. Here are the relevant fragments of the exploded graph (note that I simplified the test case, see the force-pushed commit): C forks the graph, accepting `X == 2 && (x & 8) != 0` on one of the branches: <img width="1590" height="968" alt="Screenshot from 2026-07-22 14-45-21" src="https://github.com/user-attachments/assets/c8cf13ff-e956-47df-b3dc-be501074a7df"; /> C++ evaluates `ImplicitCastExpr(IntegralToBoolean` and realizes that the `if` condition is predetermined so it does not fork: <img width="1036" height="1024" alt="Screenshot from 2026-07-22 14-45-30" src="https://github.com/user-attachments/assets/797ffa5a-0c9f-412e-8c8f-4e4551f01b85"; /> ```C++ case CK_PointerToIntegral: { SVal V = state->getSVal(Ex, SF); if (isa<nonloc::PointerToMember>(V)) { state = state->BindExpr(CastE, SF, UnknownVal()); Bldr.generateNode(CastE, Pred, state); continue; } // Explicitly proceed with default handler for this case cascade. state = handleLValueBitCast(state, Ex, SF, T, ExTy, CastE, Bldr, Pred); continue; } /// in ExprEngine::handleLValueBitCast SVal OrigV = state->getSVal(Ex, SF); SVal SimplifiedOrigV = svalBuilder.simplifySVal(state, OrigV); // <-- simplified SVal V = svalBuilder.evalCast(SimplifiedOrigV, T, ExTy); SVal V = svalBuilder.evalCast(SimplifiedOrigV, T, ExTy); ``` Both C and C++ then call `ExprEngine::processBranch` -> `assumeCondition` which ends up running `State->assume(V)` -> `ConstraintMgr->assumeDual` that produces both states where V comes from `State->getSVal(ConditionExpr)`. At which point do you expect it to simplify the symbolic expression? https://github.com/llvm/llvm-project/pull/210912 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
