Function wasm2c_marshal_and_writeback_u32_pair

src/writeback.rs:169–190

(
    ctx: &mut VmCtx,
    addr0: usize,
    addr1: usize,
    res: RuntimeResult<(u32, u32)>,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn wasm2c_marshal_and_writeback_u32_pair(
    ctx: &mut VmCtx,
    addr0: usize,
    addr1: usize,
    res: RuntimeResult<(u32, u32)>,
) -> u32 {
    if !ctx.fits_in_lin_mem_usize(addr0, 4) {
        return RuntimeError::Eoverflow.into();
    }
    if !ctx.fits_in_lin_mem_usize(addr1, 4) {
        return RuntimeError::Eoverflow.into();
    }
    //log::debug!("wasm2c_marshal_and_writeback_u32_pair: {:?}", result);
    match res {
        Ok((v0, v1)) => {
            ctx.write_u32(addr0, v0); // writeback envc
            ctx.write_u32(addr1, v1); // writeback environ_buf
            0
        }
        Err(err) => err.into(),
    }
}