Function fresh_components

src/tcb/path.rs:170–172

we should be able to solve this by knowing that length = 0

()

#[ensures(!is_symlink(&result))]
#[ensures(forall(|i: usize| (i < result.len()) ==> !is_symlink(result.prefix(i)) ))] // we should be able to solve this by knowing that length = 0
pub fn fresh_components() -> OwnedComponents {
    OwnedComponents::new()
}

#[cfg(feature = "verify")]
predicate! {