Function trace_send

src/os/mod.rs:587–598

#[ensures(effects!(old(trace), trace, effect!(FdAccess), effect!(ReadMem, addr, count)))]

(
    ctx: &mut VmCtx,
    fd: HostFd,
    ptr: SboxPtr,
    cnt: usize,
    flags: i32,
)

#[ensures(trace_safe(trace, ctx))]
// #[ensures(effects!(old(trace), trace, effect!(FdAccess), effect!(ReadMem, addr, count)))]
pub fn trace_send(
    ctx: &mut VmCtx,
    fd: HostFd,
    ptr: SboxPtr,
    cnt: usize,
    flags: i32,
) -> RuntimeResult<usize> {
    let slice = ctx.slice_mem_mut(ptr, cnt as u32);
    let os_fd: usize = fd.to_raw();
    let r = os_sendto(os_fd, slice, cnt, flags, 0, 0);
    RuntimeError::from_syscall_ret(r)
}

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