Function trace_mkdirat

src/os/mod.rs:396–406

#[ensures(two_effects!(old(trace), trace, effect!(FdAccess), effect!(PathAccessAt, os_fd)))]

(
    ctx: &VmCtx,
    dir_fd: HostFd,
    path: HostPath,
    mode: libc::mode_t,
)

#[ensures(trace_safe(trace, ctx))]
// #[ensures(two_effects!(old(trace), trace, effect!(FdAccess), effect!(PathAccessAt, os_fd)))]
pub fn trace_mkdirat(
    ctx: &VmCtx,
    dir_fd: HostFd,
    path: HostPath,
    mode: libc::mode_t,
) -> RuntimeResult<usize> {
    let os_fd: usize = dir_fd.to_raw();
    // let os_path: Vec<u8> = pathname.into();
    let r = os_mkdirat(os_fd, path, mode);
    RuntimeError::from_syscall_ret(r)
}

#[with_ghost_var(trace: &mut Trace)]
#[requires(path_safe(&pathname, false))]