Skip to main content

cursor_query_embedded

ostd::specs::mm::vm_space_embedding

Function cursor_query_embedded 

Source 
pub proof fn cursor_query_embedded<'rcu>(tracked owner: &mut CursorOwner<'rcu, UserPtConfig>)
Expand description
requires
old(owner).inv(),
ensures
final(owner).inv(),

Mirror of crate::mm::vm_space::Cursor::query / crate::mm::vm_space::CursorMut::query. The exec method internally advances the cursor; we model the position update as opaque.