Skip to main content

ArrayPtr

vstd_extra::array_ptr

Struct ArrayPtr 

Source 
pub struct ArrayPtr<V, const N: usize> {
    pub addr: usize,
    pub index: usize,
    pub _type: PhantomData<[V; N]>,
}
Expand description

Concrete representation of a pointer to an array The length of the array is not stored in the pointer

Fields§

§addr: usize§index: usize§_type: PhantomData<[V; N]>

Implementations§

Source§

impl<V, const N: usize> ArrayPtr<V, N>

Source

pub exec fn addr(&self) -> usize

returns
({ self.addr }),

Impl: cast the pointer to an integer

Source

pub exec fn from_addr(addr: usize) -> res : Self

ensures
res.addr == addr,
res.index == 0,

Impl: cast an integer to the pointer

Source

pub exec fn add(self, off: usize) -> Self

requires
self.index + off <= N,
returns
({
    Self {
        addr: self.addr,
        index: (::vstd::prelude::add(self.index, off)) as usize,
        _type: PhantomData,
    }
}),
Source§

impl<V, const N: usize> ArrayPtr<V, N>

Source

pub exec fn as_mut_ptr(&self, Tracked(perm): Tracked<&PointsTo<V, N>>) -> res : *mut V

requires
perm.wf(),
perm.is_pptr(*self),
self.index < N,
ensures
res.addr() == self.addr.wrapping_add(self.index.wrapping_mul(core::mem::size_of::<V>())),

Reconstructs a pointer to the selected array element.

Source

pub exec fn empty() -> (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)

requires
layout::size_of::<[V; N]>() > 0,
ensures
perm@.wf(),
perm@.is_pptr(res),
perm@.is_uninit_all(),
Source

pub exec fn make_as(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_uninit_all(),
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_init_all(),
forall |i: int| {
    0 <= i < N ==> final(perm).opt_value()[i] == raw_ptr::MemContents::Init(value)
},
Source

pub exec fn new(dft: V) -> (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)
where V: Copy,

requires
layout::size_of::<[V; N]>() > 0,
ensures
perm@.wf(),
perm@.is_pptr(res),
forall |i: int| {
    0 <= i < N ==> #[trigger] perm@.opt_value()[i] == raw_ptr::MemContents::Init(dft)
},
Source

pub exec fn free(self, Tracked(perm): Tracked<PointsTo<V, N>>)

requires
perm.wf(),
perm.is_pptr(self),
perm.is_uninit_all(),
Source

pub exec fn insert(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_uninit(self.index as int),
self.index < N,
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_init(self.index as int),
forall |i: int| {
    0 <= i < N && i != self.index
        ==> final(perm).opt_value()[i] == old(perm).opt_value()[i]
},
final(perm).opt_value()[self.index as int] == raw_ptr::MemContents::Init(value),

Insert value at index The value is moved into the array. Requires the slot at index to be uninitialized.

Source

pub exec fn take_at(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> res : V
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init(self.index as int),
self.index < N,
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_uninit(self.index as int),
forall |i: int| {
    0 <= i < N && i != self.index
        ==> final(perm).opt_value()[i] == old(perm).opt_value()[i]
},
res == old(perm).opt_value()[self.index as int].value(),

Take the value at index The value is moved out of the array. Requires the slot at index to be initialized. Afterwards, the slot is uninitialized.

Source

pub exec fn take_all(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> res : [V; N]

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init_all(),
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_uninit_all(),
res@ == old(perm).value(),

Take all the values of the array The values are moved out of the array. Requires all slots to be initialized. Afterwards, all slots are uninitialized.

Source

pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V, N>>) -> res : [V; N]

requires
perm.wf(),
perm.is_pptr(self),
perm.is_init_all(),
ensures
res@ == perm.value(),

Free the memory of the entire array and return the value that was previously stored in the array. Requires all slots to be initialized. Afterwards, all slots are uninitialized.

Source

pub exec fn update( &self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, index: usize, value: V, ) -> res : V
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init(index as int),
index < N,
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i]
},
final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
res == old(perm).opt_value()[index as int].value(),

Update the value at index with value and return the previous value Requires the slot at index to be initialized. Afterwards, the slot is initialized with value. Returns the previous value.

Source

pub exec fn borrow_at<'a>( &self, Tracked(perm): Tracked<&'a PointsTo<V, N>>, index: usize, ) -> res : &'a V

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
index < N,
ensures
res == perm.opt_value()[index as int].value(),

Get the reference of the value at index Borrow the immutable reference of the value at index Requires the slot at index to be initialized. Afterwards, the slot is still initialized. Returns the immutable reference of the value. The reference is valid as long as the permission is alive. The reference is not allowed to be stored.

Source

pub exec fn borrow<'a>( &self, Tracked(perm): Tracked<&'a PointsTo<V, N>>, ) -> res : &'a [V; N]

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init_all(),
ensures
forall |i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),

Get the reference of the entire array Borrow the immutable reference of the entire array Requires all slots to be initialized. Afterwards, all slots are still initialized. Returns the immutable reference of the entire array. The reference is valid as long as the permission is alive. The reference is not allowed to be stored.

Source

pub exec fn overwrite( &self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, index: usize, value: V, )

requires
old(perm).wf(),
old(perm).is_pptr(*self),
index < N,
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i]
},
final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),

Overwrite the entry at index with value The pervious value will be leaked if it was initialized.

Source

pub proof fn tracked_overwrite( tracked &self, tracked perm: &mut PointsTo<V, N>, tracked index: usize, tracked value: V, )

requires
old(perm).wf(),
old(perm).is_pptr(*self),
index < N,
ensures
final(perm).wf(),
final(perm).is_pptr(*self),
final(perm).is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> final(perm).opt_value()[i] == old(perm).opt_value()[i]
},
final(perm).opt_value()[index as int] == raw_ptr::MemContents::Init(value),
Source

pub exec fn get(&self, Tracked(perm): Tracked<&PointsTo<V, N>>, index: usize) -> res : V
where V: Copy,

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
index < N,
ensures
res == perm.opt_value()[index as int].value(),

Get the value at index and return it The value is copied from the array Requires the slot at index to be initialized. Afterwards, the slot is still initialized.

Trait Implementations§

Source§

impl<V, const N: usize> Clone for ArrayPtr<V, N>

Source§

exec fn clone(&self) -> res : Self

ensures
res == *self,
1.0.0 (const: unstable) · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl<V, const N: usize> Copy for ArrayPtr<V, N>

Auto Trait Implementations§

§

impl<V, const N: usize> Freeze for ArrayPtr<V, N>

§

impl<V, const N: usize> RefUnwindSafe for ArrayPtr<V, N>
where V: RefUnwindSafe,

§

impl<V, const N: usize> Send for ArrayPtr<V, N>
where V: Send,

§

impl<V, const N: usize> Sync for ArrayPtr<V, N>
where V: Sync,

§

impl<V, const N: usize> Unpin for ArrayPtr<V, N>
where V: Unpin,

§

impl<V, const N: usize> UnsafeUnpin for ArrayPtr<V, N>

§

impl<V, const N: usize> UnwindSafe for ArrayPtr<V, N>
where V: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

§

impl<T> Pipe for T
where T: ?Sized,

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>