Function wasm2c_marshal_and_writeback_filestat

src/writeback.rs:139–162

(
    ctx: &mut VmCtx,
    addr: usize,
    res: RuntimeResult<FileStat>,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn wasm2c_marshal_and_writeback_filestat(
    ctx: &mut VmCtx,
    addr: usize,
    res: RuntimeResult<FileStat>,
) -> u32 {
    if !ctx.fits_in_lin_mem_usize(addr, 64) {
        return RuntimeError::Eoverflow.into();
    }
    //log::debug!("wasm2c_marshal_and_writeback_filestat: {:?}", result);
    match res {
        Ok(r) => {
            ctx.write_u64(addr, r.dev);
            ctx.write_u64(addr + 8, r.ino);
            ctx.write_u64(addr + 16, r.filetype.to_wasi() as u64);
            ctx.write_u64(addr + 24, r.nlink);
            ctx.write_u64(addr + 32, r.size);
            ctx.write_u64(addr + 40, r.atim.nsec());
            ctx.write_u64(addr + 48, r.mtim.nsec());
            ctx.write_u64(addr + 56, r.ctim.nsec());
            0
        }
        Err(err) => err.into(),
    }
}

#[with_ghost_var(trace: &mut Trace)]
#[requires(ctx_safe(ctx))]