Function tracked_cursor_entry_new Copy item path

pub proof fn tracked_cursor_entry_new<'rcu>(
    vm_space: VmSpaceId,
    kind: CursorKind,
    va: Range<Vaddr>,
    tracked owner: CursorOwner<'rcu, UserPtConfig>,
    tracked guards: Guards<'rcu>,
) -> tracked res : CursorEntry<'rcu>

res.vm_space == vm_space,

res.kind == kind,

res.va == va,

res.owner == owner,

res.guards == guards,