Function expand_symlink

src/path_resolution.rs:95–116

(
    out_path: &mut OwnedComponents,
    linkpath_components: OwnedComponents,
    num_symlinks: &mut isize,
    dirfd: HostFd,
)

#[ensures(!is_symlink(out_path))]
#[ensures(forall(|i: usize| (i < out_path.len()) ==> !is_symlink(out_path.prefix(i)) ))]
fn expand_symlink(
    out_path: &mut OwnedComponents,
    linkpath_components: OwnedComponents,
    num_symlinks: &mut isize,
    dirfd: HostFd,
) {
    let mut idx = 0;
    while idx < linkpath_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))));
        if *num_symlinks >= MAXSYMLINKS {
            return;
        }
        let c = linkpath_components.lookup(idx);
        let maybe_linkpath = maybe_expand_component(dirfd, out_path, c, num_symlinks);
        if let Some(linkpath) = maybe_linkpath {
            expand_symlink(out_path, linkpath, num_symlinks, dirfd);
        }
        idx += 1;
    }
}