Struct PointsTowithDealloc

Source

pub struct PointsTowithDealloc<T> {
    pub points_to: PointsTo<T>,
    pub dealloc: Option<Dealloc>,
}

Fields§

§points_to: PointsTo<T>§dealloc: Option<Dealloc>

Implementations§

Source §

impl<T> PointsTowithDealloc<T>

Source

pub open spec fn ptr(self) -> *mut T

{ self.points_to.ptr() }

Source

pub open spec fn addr(self) -> usize

{ self.ptr().addr() }

Source

pub open spec fn is_init(self) -> bool

{ self.points_to.is_init() }

Source

pub open spec fn is_uninit(self) -> bool

{ self.points_to.is_uninit() }

Source

pub open spec fn value(self) -> T

{ self.points_to.value() }

Source

pub open spec fn dealloc_aligned(self) -> bool

{
    match self.dealloc {
        Some(dealloc) => dealloc.align() == vstd::layout::align_of::<T>(),
        None => true,
    }
}

Source

pub proof fn tracked_borrow_points_to(tracked &self) -> tracked ret : &PointsTo<T>

Source

pub proof fn tracked_get_points_to(tracked self) -> tracked ret : PointsTo<T>

Source

pub proof fn new(tracked points_to: PointsTo<T>, tracked dealloc: Option<Dealloc>) -> tracked ret : Self

requires

match dealloc {
    Some(dealloc) => (
        &&& vstd::layout::size_of::<T>() > 0
        &&& valid_layout(size_of::<T>(), dealloc.align() as usize)
        &&& points_to.ptr().addr() == dealloc.addr()
        &&& points_to.ptr()@.provenance == dealloc.provenance()
        &&& dealloc.size() == vstd::layout::size_of::<T>()

    ),
    None => vstd::layout::size_of::<T>() == 0,
},

ensures

ret.inv(),

Source

pub proof fn new_non_zero_size(tracked points_to: PointsTo<T>, tracked dealloc: Dealloc) -> tracked ret : Self

requires

0 < vstd::layout::size_of::<T>(),

valid_layout(size_of::<T>(), dealloc.align() as usize),

points_to.ptr().addr() == dealloc.addr(),

points_to.ptr()@.provenance == dealloc.provenance(),

dealloc.size() == vstd::layout::size_of::<T>() as int,

dealloc.align() == vstd::layout::align_of::<T>(),

ensures

ret.inv(),

Source

pub proof fn new_zero_size(tracked points_to: PointsTo<T>) -> tracked ret : Self

requires

vstd::layout::size_of::<T>() == 0,

ensures

ret.inv(),

Source

pub proof fn into_raw(tracked self) -> tracked ret : (PointsToRaw, Option<Dealloc>)

requires

self.inv(),

self.is_uninit(),

ensures

match ret.1 {
    Some(dealloc) => (
        &&& vstd::layout::size_of::<T>() > 0
        &&& dealloc.addr() == self.addr()
        &&& dealloc.addr() as int % vstd::layout::align_of::<T>() as int == 0
        &&& dealloc.size() == vstd::layout::size_of::<T>() as int
        &&& dealloc.provenance() == ret.0.provenance()
        &&& ret.0.is_range(dealloc.addr() as int, vstd::layout::size_of::<T>() as int)

    ),
    None => (
        &&& vstd::layout::size_of::<T>() == 0

    ),
},

Trait Implementations§

Source §

impl<T> Inv for PointsTowithDealloc<T>

Source §

open spec fn inv(self) -> bool

{
    &&& self.points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0
    &&& match self.dealloc {
        Some(dealloc) => (
            &&& vstd::layout::size_of::<T>() > 0
            &&& self.points_to.ptr().addr() == dealloc.addr()
            &&& self.points_to.ptr()@.provenance == dealloc.provenance()
            &&& dealloc.size() == vstd::layout::size_of::<T>()
            &&& valid_layout(size_of::<T>(), dealloc.align() as usize)

        ),
        None => vstd::layout::size_of::<T>() == 0,
    }

}