Skip to main content

vm_reader_skip_embedded

Function vm_reader_skip_embedded 

Source
pub proof fn vm_reader_skip_embedded(tracked owner: &mut VmIoOwner, nbytes: usize)
Expand description
requires
old(owner).inv(),
ensures
final(owner).inv(),
*final(owner) == *old(owner),

Mirror of crate::mm::io::VmReader::skip.

Exec only mutates the handle’s cursor field (no owner mutation).