Skip to main content

PermTarget

Trait PermTarget 

Source
pub trait PermTarget {
    type Value<'a>
       where Self: 'a;
    type PermPayload: ?Sized;

    // 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§

Source

type Value<'a> where Self: 'a

Value managed by the type.

For example, a pointer *const T manages a value of type T.

In practice, you will use a borrow &'a T here, to allow for unsized types.

Source

type PermPayload: ?Sized

Variance, objectiveness and sizeness parametrization for the Perm.

This type is used to force certain auto-traits to be implemented on the Perm object (or not!). See this trait implementation for PermCell for an example. You may also add a type like [bool] to force unsizeness.

Provided Methods§

Source

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 != other

Dyn 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

Source§

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()
Source§

type Value<'a> = &'a T where Self: 'a

Source§

type PermPayload = (NotObjective, PhantomData<T>, [bool])

Implementors§

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicBool

Source§

type Value<'a> = FMap<Int, (bool, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicBool

Source§

type Value<'a> = bool where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicI8

Source§

type Value<'a> = FMap<Int, (i8, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicI8

Source§

type Value<'a> = i8 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicI16

Source§

type Value<'a> = FMap<Int, (i16, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicI16

Source§

type Value<'a> = i16 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicI32

Source§

type Value<'a> = FMap<Int, (i32, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicI32

Source§

type Value<'a> = i32 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicI64

Source§

type Value<'a> = FMap<Int, (i64, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicI64

Source§

type Value<'a> = i64 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicIsize

Source§

type Value<'a> = FMap<Int, (isize, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicIsize

Source§

type Value<'a> = isize where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicU8

Source§

type Value<'a> = FMap<Int, (u8, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicU8

Source§

type Value<'a> = u8 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicU16

Source§

type Value<'a> = FMap<Int, (u16, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicU16

Source§

type Value<'a> = u16 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicU32

Source§

type Value<'a> = FMap<Int, (u32, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicU32

Source§

type Value<'a> = u32 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicU64

Source§

type Value<'a> = FMap<Int, (u64, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicU64

Source§

type Value<'a> = u64 where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic::AtomicUsize

Source§

type Value<'a> = FMap<Int, (usize, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl PermTarget for creusot_std::std::sync::atomic_sc::AtomicUsize

Source§

type Value<'a> = usize where Self: 'a

Source§

type PermPayload = ()

Source§

impl<T: ?Sized> PermTarget for PermCell<T>

Source§

type Value<'a> = &'a T where Self: 'a

Source§

type PermPayload = (NotObjective, PhantomData<T>)

Source§

impl<T> PermTarget for creusot_std::std::sync::atomic::AtomicPtr<T>

Source§

type Value<'a> = FMap<Int, (*mut T, SyncView)> where Self: 'a

Source§

type PermPayload = ()

Source§

impl<T> PermTarget for creusot_std::std::sync::atomic_sc::AtomicPtr<T>

Source§

type Value<'a> = *mut T where Self: 'a

Source§

type PermPayload = ()