transform_constant_expr

charon_lib::transform::simplify_output::simplify_constants

Function transform_constant_expr 

Source 
fn transform_constant_expr(
    ctx: &mut UllbcStatementTransformCtx<'_>,
    val: Box<ConstantExpr>,
) -> Operand
Expand description

If the constant value is a constant ADT, push Assign::Aggregate statements to the vector of statements, that bind new variables to the ADT parts and the variable assigned to the complete ADT.

Goes fom e.g. f(T::A(x, y)) to let a = T::A(x, y); f(a). The function is recursively called on the aggregate fields (e.g. here x and y).