pub unsafe trait AnyFrameMeta {
// Required method
spec fn vtable_ptr(&self) -> usize
where Self: Sized;
// Provided methods
open spec fn on_drop_pre(
&self,
reader: VmReader<'_, Infallible>,
regions: MetaRegionOwners,
vm_io_owner: VmIoOwner,
) -> bool { ... }
fn on_drop(
&mut self,
_reader: &mut VmReader<'_, Infallible>,
verus_tmp__regions: Tracked<&mut MetaRegionOwners>,
verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>,
) { ... }
fn is_untyped(&self) -> bool { ... }
}Expand description
Space-holder of the AnyFrameMeta virtual table.
Dyn-compatible: no Self-by-value, no associated types on dispatched
methods, no dyn-incompatible supertrait. vtable_ptr is Self: Sized
because it’s only used statically (the runtime vtable pointer lives on
the slot, not on the instance). Sites that need Repr<MetaSlotStorage>
must spell it out — it was previously a supertrait.
Required Methods§
Sourcespec fn vtable_ptr(&self) -> usizewhere
Self: Sized,
spec fn vtable_ptr(&self) -> usizewhere
Self: Sized,
Provided Methods§
Sourceopen spec fn on_drop_pre(
&self,
reader: VmReader<'_, Infallible>,
regions: MetaRegionOwners,
vm_io_owner: VmIoOwner,
) -> bool
open spec fn on_drop_pre( &self, reader: VmReader<'_, Infallible>, regions: MetaRegionOwners, vm_io_owner: VmIoOwner, ) -> bool
{ true }Per-impl precondition for Self::on_drop. Default is true.
Impls that need richer caller-side invariants (e.g. the PT-node’s
reader/region invariants) override this; the trait method’s
requires clause calls it.
Sourceexec fn on_drop(
&mut self,
_reader: &mut VmReader<'_, Infallible>,
verus_tmp__regions: Tracked<&mut MetaRegionOwners>,
verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>,
)
exec fn on_drop( &mut self, _reader: &mut VmReader<'_, Infallible>, verus_tmp__regions: Tracked<&mut MetaRegionOwners>, verus_tmp__vm_io_owner: Tracked<&mut VmIoOwner>, )
old(_regions).inv(),old(_reader).inv(),old(_vm_io_owner).inv(),old(_reader).wf(*old(_vm_io_owner)),old(self).on_drop_pre(*old(_reader), *old(_regions), *old(_vm_io_owner)),final(_regions).inv(),final(_reader).inv(),final(_vm_io_owner).inv(),final(_reader).wf(*final(_vm_io_owner)),Sourceexec fn is_untyped(&self) -> bool
exec fn is_untyped(&self) -> bool
Implementors§
impl AnyFrameMeta for MetaSlotStorage
MetaSlotStorage is an inductive tagged union of all of the frame meta types that
we work with in this development. So, it should itself implement AnyFrameMeta, and
it can then be used to stand in for dyn AnyFrameMeta.