Function trace_fgetfl

src/os/mod.rs:332–336

(ctx: &VmCtx, fd: HostFd)

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

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