Commit d8a8224
committed
Verify safety of slice iterator functions (Challenge 18)
Add verification harnesses for all Part 1 and Part 2 functions required
by Challenge 18. This includes:
Part 1 (macros.rs iterator! functions):
- All 16 macro-generated functions (make_slice, len, is_empty, next,
size_hint, count, nth, advance_by, last, fold, for_each, position,
rposition, next_back, nth_back, advance_back_by) verified for both
Iter and IterMut across 4 representative types ((), u8, char, (char,u8))
Part 2 (iter.rs):
- 9 __iterator_get_unchecked contracts verified (Windows, Chunks,
ChunksMut, ChunksExact, ChunksExactMut, RChunks, RChunksMut,
RChunksExact, RChunksExactMut)
- 33 safe functions with unsafe code verified (Iter::new, IterMut::new/
into_slice/as_mut_slice, Split::next/next_back, all Chunks/ChunksExact/
RChunks/RChunksExact variants, ArrayWindows next/nth/next_back/nth_back)
Uses #[cfg(kani)] abstractions in macros.rs for fold/for_each/position/
rposition to enable unbounded verification of loop-based functions.1 parent 9bbdb30 commit d8a8224
2 files changed
Lines changed: 1029 additions & 101 deletions
0 commit comments