Enum PropertyContract 

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

A parsed safety-property contract.

The variants correspond to the primitive safety-property tags used by the annotation DSL and the built-in standard-library contract database.

Variants

Align(Ty<'tcx>)

Alignment requirement for a pointer interpreted as Ty.

Size()

Size requirement placeholder.

NoPadding

No-padding layout requirement placeholder.

NonNull

Non-null pointer requirement.

Allocated(Ty<'tcx>, ContractExpr<'tcx>)

Allocation provenance requirement for Ty and length.

InBound(Ty<'tcx>, ContractExpr<'tcx>)

Object-boundary requirement for Ty and length.

NonOverlap

Non-overlapping memory range requirement placeholder.

ValidNum(Vec<NumericPredicate<'tcx>>)

Numeric relationship requirements.

ValidString

UTF-8 string validity requirement placeholder.

ValidCStr

NUL-terminated C string validity requirement placeholder.

Init(Ty<'tcx>, ContractExpr<'tcx>)

Initialization requirement for Ty and length.

Unwrap

Option/Result unwrap safety requirement placeholder.

Typed(Ty<'tcx>)

Dynamic type compatibility requirement.

Owning

Ownership requirement placeholder.

Alias

Aliasing requirement placeholder.

Alive

Liveness requirement placeholder.

Pinned

Pinning requirement placeholder.

NonVolatile

Non-volatile access requirement placeholder.

Opened

Resource-open state requirement placeholder.

Trait

Trait invariant requirement placeholder.

Unreachable

Unreachable-code contract placeholder.

ValidPtr(Ty<'tcx>, ContractExpr<'tcx>)

Composite valid-pointer requirement.

Deref

Dereferenceability requirement placeholder.

Ptr2Ref

Pointer-to-reference conversion requirement placeholder.

Layout

Layout compatibility requirement placeholder.

Unknown

Unknown or currently unsupported safety-property tag.

Implementations

impl<'tcx> PropertyContract<'tcx>

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

Parse one safety-property tag from the annotation DSL.

pub fn new_partial_order(lhs: usize, rhs: usize, op: MirBinOp) -> Self

Create a numeric partial-order contract between two MIR locals.

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

Create the default object-boundary contract for a newly modeled object.

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

Validate the number of parsed annotation arguments.

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

Parse a type argument from a contract expression.

fn parse_target_type( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, ) -> Option<Ty<'tcx>>

Parse the current type of a target place used by a two-argument contract form.

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

Parse any numeric expression used by a contract.

fn parse_contract_place( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, ) -> Option<ContractPlace<'tcx>>

Parse a place expression from an annotation expression.

fn parse_arg_place(expr: &Expr) -> Option<ContractPlace<'tcx>>

Parse contract argument references such as Arg_1.

fn parse_valid_num( tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &Vec<Expr>, ) -> Vec<NumericPredicate<'tcx>>

Parse ValidNum into one or more numeric predicates.

fn parse_numeric_predicate( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, ) -> Option<NumericPredicate<'tcx>>

Parse a single comparison predicate, falling back to expr != 0.

fn parse_interval_predicates( tcx: TyCtxt<'tcx>, def_id: DefId, value: &Expr, range: &Expr, ) -> Option<Vec<NumericPredicate<'tcx>>>

Parse interval-style ValidNum(value, [lower, upper]) predicates.

fn parse_string_interval( tcx: TyCtxt<'tcx>, def_id: DefId, value: &Expr, raw_range: &str, ) -> Option<Vec<NumericPredicate<'tcx>>>

Parse string interval notation such as "[0,self.len)".

fn build_interval_predicates( tcx: TyCtxt<'tcx>, def_id: DefId, value: &Expr, lower: &Expr, lower_inclusive: bool, upper: &Expr, upper_inclusive: bool, ) -> Vec<NumericPredicate<'tcx>>

Build lower/upper bound predicates for an interval contract.

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.