Skip to main content

checked_mul_guard_branch_model

foundry_evm_symbolic::runtime::solver::fallback

Function checked_mul_guard_branch_model 

Source 
pub(super) fn checked_mul_guard_branch_model(
    cx: &SymCx,
    constraints: &[SymBoolExpr],
    original_constraints: &[SymBoolExpr],
    replayable_storage: &IndexSet<Symbol>,
) -> Option<HashMap<Symbol, U256>>
Expand description

Constructs and validates a concrete model for a checked-multiply guard branch.

Solidity’s guard is x == 0 || (x * y) / x == y. The assignments below represent its semantic cases directly: the zero disjunct, a nonzero exact product, and wrapping products in either operand order. Simple support constraints are completed first so an exact operand value from the path is preserved instead of being overwritten by the semantic default. This does not perform the generic bounded candidate search, and a model is returned only when it satisfies every original constraint.