Skip to content

INVENTORY.md

Latest commit

 

History

History
19 lines (16 loc) · 834 Bytes

INVENTORY.md

File metadata and controls

19 lines (16 loc) · 834 Bytes
Raw

Inventory

Potential Removals

  • None at the moment.

Desired Functionality

  • Add Kani proofs for winnow view helpers.
  • Add test covering freezing an empty section to guard against flush errors on macOS.
  • Explore how to model ByteArea for Kani or fuzzing without depending on OS-backed memory maps.

Discovered Issues

  • Bytes::from_source with Box<T> triggers a Stacked Borrows violation because moving the Box invalidates prior tags on its heap allocation. This is a known limitation of Stacked Borrows with Box; Tree Borrows handles it correctly. The Miri tests use Tree Borrows (-Zmiri-tree-borrows) accordingly.
  • The test_winnow_view_parser test fails under Miri because it assumes the Vec<u8> allocation is 2-byte aligned for a u16-containing struct; Miri doesn't guarantee this alignment.