pub trait PermTarget {
type Value: ?Sized;
type Objectiveness;
// Provided method
fn is_disjoint(
&self,
_self_val: &Self::Value,
other: &Self,
_other_val: &Self::Value,
) -> bool { ... }
}Expand description
Trait for the types that can be used in a Perm.
Required Associated Types§
Sourcetype Value: ?Sized
type Value: ?Sized
Value managed by the type.
For example, a pointer *const T manages a value of type T.
Sourcetype Objectiveness
type Objectiveness
Objectiveness parametrization for the Perm.
This type is used to force the Objective
auto-trait to be implemented on the Perm object (or not!). See
this trait implementation for
PermCell for an example.
Provided Methods§
Sourcefn is_disjoint(
&self,
_self_val: &Self::Value,
other: &Self,
_other_val: &Self::Value,
) -> bool
fn is_disjoint( &self, _self_val: &Self::Value, other: &Self, _other_val: &Self::Value, ) -> bool
Logical function that describes the behavior of Perm::disjoint_lemma.
logic(open, inline)
self != otherDyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".
Implementations on Foreign Types§
Source§impl<T: ?Sized> PermTarget for *const T
impl<T: ?Sized> PermTarget for *const T
Source§fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool
fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool
Two pointers to distinct non-empty allocations are disjoint.
Note that this definition also implies that a pointer to a ZST is disjoint with itself.
logic(open, inline)
size_of_val_logic(*self_val) != 0 && size_of_val_logic(*other_val) != 0 ==> self.addr_logic() != other.addr_logic()