charon_lib::transform::index_to_function_calls

Function compute_subslice_end_idx

Source 
pub fn compute_subslice_end_idx<T: BodyTransformCtx>(
    ctx: &mut T,
    len_place: &Place,
    last_arg: Operand,
    from_end: bool,
) -> Operand
Expand description

When from_end is true, we need to compute len(p) - last_arg instead of just using last_arg. Otherwise, we simply return last_arg. New local variables are created as needed.

The last_arg is either the offset for Index or the to for Subslice for the projections.