Struct Property 

pub struct Property<'tcx> {
    pub kind: PropertyKind,
    pub args: Vec<PropertyArg<'tcx>>,
}

Fields

kind: PropertyKind

args: Vec<PropertyArg<'tcx>>

Implementations

impl<'tcx> Property<'tcx>

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

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

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

fn new_simple(kind: PropertyKind) -> Self

fn new_with_args(kind: PropertyKind, args: Vec<PropertyArg<'tcx>>) -> Self

fn new_with_target( kind: PropertyKind, tcx: TyCtxt<'tcx>, def_id: DefId, exprs: &[Expr], ) -> 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_target_type( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, ) -> Option<Ty<'tcx>>

fn parse_target_arg( tcx: TyCtxt<'tcx>, def_id: DefId, expr: &Expr, ) -> PropertyArg<'tcx>

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

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

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

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

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

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

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

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

Trait Implementations

impl<'tcx> Clone for Property<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for Property<'tcx>

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

Formats the value using the given formatter.