Function first_null

src/tcb/misc.rs:151–156

(buf: &Vec<u8>, start: usize, offset: usize, len: usize)

#[requires(buf.len() >= start + len)]
#[ensures(result < old(len))]
pub fn first_null(buf: &Vec<u8>, start: usize, offset: usize, len: usize) -> usize {
    buf[start + offset..start + len]
        .iter()
        .position(|x| *x == 0)
        .unwrap()
}

#[trusted]
// #[requires(buf.len() > start + len + 19)]