Skip to main content

cursor_mut_map_embedded

ostd::specs::mm::vm_space_embedding

Function cursor_mut_map_embedded 

Source 
pub proof fn cursor_mut_map_embedded<'rcu>(tracked 
    owner: &mut CursorOwner<'rcu, UserPtConfig>,
tracked     regions: &mut MetaRegionOwners,
    frame: UFrame,
    prop: PageProperty,
)
Expand description
requires
old(owner).inv(),
old(regions).inv(),
ensures
final(owner).inv(),
final(regions).inv(),

Mirror of crate::mm::vm_space::CursorMut::map.

Modifies both the cursor owner and MetaRegionOwners.