Struct ContractualInvariantState

pub struct ContractualInvariantState<'tcx> {
    pub contracts: Vec<PropertyContract<'tcx>>,
}

Fields

contracts: Vec<PropertyContract<'tcx>>

Implementations

impl<'tcx> ContractualInvariantState<'tcx>

pub fn new_default() -> Self

pub fn add_contract(&mut self, contract: PropertyContract<'tcx>)

pub fn get_contracts_length(&self) -> usize

Trait Implementations

impl<'tcx> Clone for ContractualInvariantState<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for ContractualInvariantState<'tcx>

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

Formats the value using the given formatter.