Pod

ostd::mm::pod

Trait Pod 

Source 
pub trait Pod: Copy + Sized {
    // Provided methods
    exec fn new_zeroed() -> Self { ... }
    fn new_uninit() -> Self { ... }
    fn as_bytes<const N: usize>(
        &self,
    ) -> (ArrayPtr<u8, N>, Tracked<&PointsTo<u8, N>>) { ... }
    fn as_bytes_mut(&mut self) -> (usize, usize) { ... }
}
Expand description

A trait for Plain Old Data (POD) types.

Provided Methods§

Source

exec fn new_zeroed() -> Self

Creates a new instance of Pod type that is filled with zeroes.

Source

exec fn new_uninit() -> Self

Creates a new instance of Pod type with uninitialized content.

Source

exec fn as_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.

Source

exec fn as_bytes_mut(&mut self) -> r : (usize, usize)

ensures
r.1 == core::mem::size_of::<Self>(),

As a mutable slice of bytes.

Note that this does not create the permission to mutate the Pod value as mutable reference is not yet supported in Verus.

Instead, the caller must uphold a separate permission to mutate the Pod value.

This seems a bit awkward if we try to use arrayptr and then making a mutable reference from it as verus cannot do it now.

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§