Function expand_path

src/path_resolution.rs:27–60

(vec: Vec<u8>, should_follow: bool, dirfd: HostFd)

    }
)]
fn expand_path(vec: Vec<u8>, should_follow: bool, dirfd: HostFd) -> RuntimeResult<OwnedComponents> {
    let p = to_pathbuf(vec);
    let components = get_components(&p);

    let mut out_path = fresh_components();
    let mut num_symlinks = 0;
    let mut idx = 0;

    while idx < components.len() {
        body_invariant!(!is_symlink(&out_path));
        // out_path should never contain symlinks
        body_invariant!(forall(|i: usize| i < out_path.len() ==> !is_symlink(out_path.prefix(i)) ) );
        let comp = components[idx];
        let c = OwnedComponent::from_borrowed(&comp);
        // if this is the last element, and we are NO_FOLLOW, then don't expand
        if !should_follow && idx + 1 == components.len() {
            out_path.push(c);
            break;
        }
        // if comp is a symlink, return path + update num_symlinks
        // if not, just extend out_path
        let maybe_linkpath = maybe_expand_component(dirfd, &mut out_path, c, &mut num_symlinks);

        if let Some(linkpath) = maybe_linkpath {
            expand_symlink(&mut out_path, linkpath, &mut num_symlinks, dirfd);
        }
        if num_symlinks >= MAXSYMLINKS {
            return Err(RuntimeError::Eloop);
        }
        idx += 1;
    }
    //assert!(!should_follow || (should_follow && !is_symlink(&out_path)));
    Ok(out_path)
}

#[ensures(
    match &result {