pub trait Pod: Copy + Sized {
// Provided methods
exec fn new_zeroed() -> Self { ... }
fn new_uninit() -> Self { ... }
fn as_array_ptr_bytes<const N: usize>(
&self,
) -> (ArrayPtr<u8, N>, Tracked<&PointsTo<u8, N>>) { ... }
fn as_bytes_mut(&mut self) -> &mut [u8] ⓘ { ... }
fn as_bytes(&self) -> &[u8] ⓘ { ... }
}Expand description
A trait for Plain Old Data (POD) types.
Provided Methods§
Sourceexec fn new_zeroed() -> Self
exec fn new_zeroed() -> Self
Creates a new instance of Pod type that is filled with zeroes.
Sourceexec fn new_uninit() -> Self
exec fn new_uninit() -> Self
Creates a new instance of Pod type with uninitialized content.
Sourceexec fn as_array_ptr_bytes<const N: usize>(
&self,
) -> slice : (ArrayPtr<u8, N>, Tracked<&PointsTo<u8, N>>)
exec fn as_array_ptr_bytes<const N: usize>( &self, ) -> slice : (ArrayPtr<u8, N>, Tracked<&PointsTo<u8, N>>)
ensures
slice.1@.value().len() == core::mem::size_of::<Self>(),slice.1@.wf(),slice.0.addr() == slice.1@.addr(),As a slice of bytes via an [ArrayPtr] (with a tracked permission).
This is the verus-flavored variant; the raw &[u8] view is Self::as_bytes.
Sourceexec fn as_bytes_mut(&mut self) -> r : &mut [u8] ⓘ
exec fn as_bytes_mut(&mut self) -> r : &mut [u8] ⓘ
ensures
r.len() == core::mem::size_of::<Self>(),As a mutable slice of bytes.
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.