#[requires(buf.len() > start + len + 19)]
(out_buf: &mut Vec<u8>, buf: &Vec<u8>, start: usize, len: usize)
| 158 | #[trusted] |
| 159 | // #[requires(buf.len() > start + len + 19)] |
| 160 | pub fn push_dirent_name(out_buf: &mut Vec<u8>, buf: &Vec<u8>, start: usize, len: usize) { |
| 161 | out_buf.extend_from_slice(&buf[start..start + len]) |
| 162 | } |
| 163 | |
| 164 | // Trusted because I need to convince prusti that clone does not alter |
| 165 | // the length of vectors |
no outgoing calls
no test coverage detected