Function trace_preadv

src/os/mod.rs:145–157

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

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

#[with_ghost_var(trace: &mut Trace)]
#[requires(ctx.fits_in_lin_mem(ptr, cnt as u32, trace))]