pub trait RCClone: Sized {
// Required methods
spec fn clone_requires(
self,
slot_perm: PointsTo<MetaSlot>,
rc_perm: PermissionU64,
) -> bool;
exec fn clone(
&self,
verus_tmp_slot_perm: Tracked<&PointsTo<MetaSlot>>,
verus_tmp_rc_perm: Tracked<&mut PermissionU64>,
) -> res : Self;
}Required Methods§
Sourcespec fn clone_requires(
self,
slot_perm: PointsTo<MetaSlot>,
rc_perm: PermissionU64,
) -> bool
spec fn clone_requires( self, slot_perm: PointsTo<MetaSlot>, rc_perm: PermissionU64, ) -> bool
Sourceexec fn clone(
&self,
verus_tmp_slot_perm: Tracked<&PointsTo<MetaSlot>>,
verus_tmp_rc_perm: Tracked<&mut PermissionU64>,
) -> res : Self
exec fn clone( &self, verus_tmp_slot_perm: Tracked<&PointsTo<MetaSlot>>, verus_tmp_rc_perm: Tracked<&mut PermissionU64>, ) -> res : Self
requires
self.clone_requires(*slot_perm, *old(rc_perm)),old(rc_perm).is_for(slot_perm.value().ref_count),old(rc_perm).value() < u64::MAX,res == *self,rc_perm.value() == old(rc_perm).value() + 1,rc_perm.id() == old(rc_perm).id(),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.