Function min_depth

src/tcb/path.rs:105–130

(components: &OwnedComponents)

#[pure]
#[trusted]
pub fn min_depth(components: &OwnedComponents) -> isize {
    let mut curr_depth = 0;
    let mut idx = 0;
    while idx < components.len() {
        body_invariant!(curr_depth >= 0);
        match components.lookup(idx) {
            OwnedComponent::RootDir => {
                return DEPTH_ERR;
            } // hacky, but fine for now
            OwnedComponent::CurDir => {}
            OwnedComponent::ParentDir => {
                curr_depth -= 1;
            }
            OwnedComponent::Normal(_) => {
                curr_depth += 1;
            }
        };
        // if curr_depth ever dips below 0, it is illegal
        // this prevents paths like ../other_sandbox_home
        if curr_depth < 0 {
            return curr_depth;
        }
        idx += 1;
    }
    curr_depth
}

#[trusted]
#[ensures(result.is_none() ==> old(!is_symlink(out_path)) )]