Type Alias UFrame 

pub type UFrame = Frame<MetaSlotStorage>;

A smart pointer to an untyped frame with any metadata.

The metadata of the frame is not known at compile time but the frame must be an untyped one. An UFrame as a parameter accepts any type of untyped frame metadata.

The usage of this frame will not be changed while this object is alive. Verus doesn’t let us do very much with dyn traits, so instead of a dyn AnyFrameMeta we use MetaSlotStorage, a type that is a tagged union of the metadata types we’ve worked with so far.

Aliased Type

pub struct UFrame {
    pub ptr: PPtr<MetaSlot>,
    pub _marker: PhantomData<MetaSlotStorage>,
    pub tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>,
    pub tracked_metadata_perm: Tracked<Option<Count<MetadataPerm, 9223372036854775807>>>,
}

Fields

ptr: PPtr<MetaSlot>

_marker: PhantomData<MetaSlotStorage>

tracked_slot_perm: Tracked<&'static PointsTo<MetaSlot>>

The permission to access the MetaSlot fields.

tracked_metadata_perm: Tracked<Option<Count<MetadataPerm, 9223372036854775807>>>

One fractional permission for the currently installed metadata.

Trait Implementations

impl<M: AnyUFrameMeta> From<Frame<M>> for UFrame

exec fn from(frame: Frame<M>) -> Self