Function trace_datasync

src/os/mod.rs:288–292

(ctx: &VmCtx, fd: HostFd)

#[ensures(trace_safe(trace, ctx))]
#[ensures(effects!(old(trace), trace, effect!(FdAccess)))]
pub fn trace_datasync(ctx: &VmCtx, fd: HostFd) -> RuntimeResult<usize> {
    let os_fd: usize = fd.to_raw();
    let r = os_fdatasync(os_fd);
    RuntimeError::from_syscall_ret(r)
}

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