Enum PropertyContract 

pub enum PropertyContract<'tcx> {
    Align(Ty<'tcx>),
    Size(),
    NoPadding,
    NonNull,
    Allocated(Ty<'tcx>, CisRangeItem),
    InBound(Ty<'tcx>, CisRangeItem),
    NonOverlap,
    ValidNum(CisRange),
    ValidString,
    ValidCStr,
    Init(Ty<'tcx>, CisRangeItem),
    Unwrap,
    Typed(Ty<'tcx>),
    Owning,
    Alias,
    Alive,
    Pinned,
    NonVolatile,
    Opened,
    Trait,
    Unreachable,
    ValidPtr(Ty<'tcx>, CisRangeItem),
    Deref,
    Ptr2Ref,
    Layout,
    Unknown,
}

Variants

Align(Ty<'tcx>)

Size()

NoPadding

NonNull

Allocated(Ty<'tcx>, CisRangeItem)

InBound(Ty<'tcx>, CisRangeItem)

NonOverlap

ValidNum(CisRange)

ValidString

ValidCStr

Init(Ty<'tcx>, CisRangeItem)

Unwrap

Typed(Ty<'tcx>)

Owning

Alias

Alive

Pinned

NonVolatile

Opened

Trait

Unreachable

ValidPtr(Ty<'tcx>, CisRangeItem)

Deref

Ptr2Ref

Layout

Unknown

Implementations

impl<'tcx> PropertyContract<'tcx>

pub fn new( tcx: TyCtxt<'tcx>, def_id: DefId, name: &str, exprs: &Vec<Expr>, ) -> Self

pub fn new_patial_order(p: usize, op: BinOp) -> Self

pub fn new_obj_boundary(ty: Ty<'tcx>, len: CisRangeItem) -> Self

fn check_arg_length(expr_len: usize, required_len: usize, sp: &str) -> bool

fn parse_type( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str, ) -> Ty<'tcx>

fn parse_length( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, sp: &str, ) -> CisRangeItem

Trait Implementations

impl<'tcx> Clone for PropertyContract<'tcx>

fn clone(&self) -> PropertyContract<'tcx>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for PropertyContract<'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.