Struct LeafProperty 

pub struct LeafProperty<'tcx> {
    pub kind: PropertyKind,
    pub args: Vec<PropertyArg<'tcx>>,
    pub contract_kind: ContractKind,
    pub null_guard: Option<PlaceKey>,
    pub for_each: Option<ContractPlace<'tcx>>,
    pub origin_name: Option<String>,
    pub origin_args: Option<Vec<String>>,
    pub origin_meaning: Option<String>,
}

Fields

kind: PropertyKind

args: Vec<PropertyArg<'tcx>>

contract_kind: ContractKind

null_guard: Option<PlaceKey>

When set, this property came from an any(Null(guard), ...) expansion and is vacuously true when guard is null.

for_each: Option<ContractPlace<'tcx>>

When set, this property must hold for every element of this container (e.g. Owning(buckets.iter())). The target place in args is already stripped of the IterElements projection and refers to a single element slot.

origin_name: Option<String>

When set, the display name of the compound def this property expanded from (e.g. "Deref", "ValidPtr"), used for user-facing reports so a macro-expanded contract keeps its original name.

origin_args: Option<Vec<String>>

The full call-site arguments of the compound def (rendered as source text), used to display name(args) as a single entry.

origin_meaning: Option<String>

The human-readable meaning of the compound def, sourced from its /// doc comment.

Trait Implementations

impl<'tcx> Clone for LeafProperty<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for LeafProperty<'tcx>

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

Formats the value using the given formatter.