Skip to main content

RCClone

ostd::mm::page_table

Trait RCClone 

Source 
pub trait RCClone: Sized {
    // Required methods
    spec fn clone_requires(self, perm: MetaRegionOwners) -> bool;
    spec fn clone_ensures(
        self,
        old_perm: MetaRegionOwners,
        new_perm: MetaRegionOwners,
        res: Self,
    ) -> bool;
    exec fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> res : Self;
}

Required Methods§

Source

spec fn clone_requires(self, perm: MetaRegionOwners) -> bool

Source

spec fn clone_ensures( self, old_perm: MetaRegionOwners, new_perm: MetaRegionOwners, res: Self, ) -> bool

Source

exec fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> res : Self

requires
self.clone_requires(*old(perm)),
ensures
res == *self,
self.clone_ensures(*old(perm), *final(perm), res),
final(perm).inv(),
final(perm).slots == old(perm).slots,
final(perm).slot_owners.dom() == old(perm).slot_owners.dom(),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§