Function trace_writev

src/os/mod.rs:192–203

(
    ctx: &mut VmCtx,
    fd: HostFd,
    iovs: &WasmIoVecs,
    iovcnt: usize,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn trace_writev(
    ctx: &mut VmCtx,
    fd: HostFd,
    iovs: &WasmIoVecs,
    iovcnt: usize,
) -> RuntimeResult<usize> {
    let native_iovs = ctx.translate_iovs(iovs);
    // native_iovs
    let os_fd: usize = fd.to_raw();
    let r = os_writev(os_fd, &native_iovs, iovcnt);
    RuntimeError::from_syscall_ret(r)
}

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