ostd::mm::frame::linked_list

Struct CursorMut

pub struct CursorMut<M: AnyFrameMeta + Repr<MetaSlot>> {
    pub list: PPtr<LinkedList<M>>,
    pub current: Option<ReprPtr<MetaSlot, Link<M>>>,
}

Expand description

A cursor that can mutate the linked list links.

The cursor points to either a frame or the “ghost” non-element. It points to the “ghost” non-element when the cursor surpasses the back of the list.

Fields§

§list: PPtr<LinkedList<M>>§current: Option<ReprPtr<MetaSlot, Link<M>>>

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorMut<M>

Source

pub exec fn move_next(&mut self)

with

Tracked(owner): Tracked <CursorOwner <M>>,

requires

owner.inv(),

old(self).wf(owner),

ensures

self.model(owner.move_next_owner_spec()) == old(self).model(owner).move_next_spec(),

owner.move_next_owner_spec().inv(),

self.wf(owner.move_next_owner_spec()),

Moves the cursor to the next frame towards the back.

If the cursor is pointing to the “ghost” non-element then this will move it to the first element of the LinkedList. If it is pointing to the last element of the LinkedList then this will move it to the “ghost” non-element.

Source

pub exec fn move_prev(&mut self)

with

Tracked(owner): Tracked <CursorOwner <M>>,

requires

owner.inv(),

old(self).wf(owner),

ensures

self.model(owner.move_prev_owner_spec()) == old(self).model(owner).move_prev_spec(),

owner.move_prev_owner_spec().inv(),

self.wf(owner.move_prev_owner_spec()),

Moves the cursor to the previous frame towards the front.

If the cursor is pointing to the “ghost” non-element then this will move it to the last element of the LinkedList. If it is pointing to the first element of the LinkedList then this will move it to the “ghost” non-element.

Source

pub exec fn take_current( &mut self, ) -> res : Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(owner): Tracked <& mut CursorOwner <M>>,

requires

old(self).wf(*old(owner)),

old(owner).inv(),

old(regions).inv(),

old(owner).length() > 0
    ==> old(regions)
        .slots
        .contains_key(frame_to_index(old(self).current.unwrap().addr())),

ensures

old(owner).length() == 0 ==> res.is_none(),

res.is_some()
    ==> res.unwrap().0.model(res.unwrap().1@).meta
        == old(owner).list_own.list[old(owner).index]@,

res.is_some() ==> self.model(*owner) == old(self).model(*old(owner)).remove(),

res.is_some() ==> res.unwrap().1@.frame_link_inv(),

Takes the current pointing frame out of the linked list.

If successful, the frame is returned and the cursor is moved to the next frame. If the cursor is pointing to the back of the list then it is moved to the “ghost” non-element.

Source

pub exec fn insert_before(&mut self, frame: UniqueFrame<Link<M>>)

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(owner): Tracked <& mut CursorOwner <M>>,
Tracked(frame_own): Tracked <& mut UniqueFrameOwner <Link <M>>>,

requires

old(self).wf(*old(owner)),

old(owner).inv(),

old(owner).list_own.list_id != 0,

old(frame_own).inv(),

old(frame_own).global_inv(*old(regions)),

frame.wf(*old(frame_own)),

old(owner).length() < usize::MAX,

old(regions).inv(),

old(regions).slots.contains_key(old(frame_own).slot_index),

old(regions)
    .slot_owners[old(frame_own).slot_index]
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),

old(frame_own).meta_perm.addr() == frame.ptr.addr(),

old(frame_own).frame_link_inv(),

ensures

self.model(*owner) == old(self).model(*old(owner)).insert(frame_own.meta_own@),

self.wf(*owner),

owner.inv(),

Inserts a frame before the current frame.

If the cursor is pointing at the “ghost” non-element then the new element is inserted at the back of the LinkedList.

Source

pub exec fn as_list(&self) -> PPtr<LinkedList<M>>

Provides a reference to the linked list.

Trait Implementations§

Source §

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& 0 <= owner.index < owner.length()
        ==> self.current.is_some()
            && self.current.unwrap().addr() == owner.list_own.list[owner.index].paddr
            && owner.list_own.perms[owner.index].pptr() == self.current.unwrap()
    &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
    &&& owner.list_perm.pptr() == self.list
    &&& owner.list_perm.is_init()
    &&& owner.list_perm.mem_contents().value().wf(owner.list_own)

}

Source §