Function trace_openat

src/os/mod.rs:29–38

#[ensures(one_effect!(old(trace), trace, effect!(PathAccessAt, os_fd, p)))]

(
    ctx: &VmCtx,
    dir_fd: HostFd,
    path: HostPath,
    flags: i32,
)

#[ensures(trace_safe(trace, ctx))]
// #[ensures(one_effect!(old(trace), trace, effect!(PathAccessAt, os_fd, p)))]
pub fn trace_openat(
    ctx: &VmCtx,
    dir_fd: HostFd,
    path: HostPath,
    flags: i32,
) -> RuntimeResult<usize> {
    let os_fd: usize = dir_fd.to_raw();
    let r = os_openat(os_fd, path, flags, 0o666);
    RuntimeError::from_syscall_ret(r)
}

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