Struct ContractFactSet 

pub struct ContractFactSet<'tcx> {
    pub contracts: Vec<PropertyContract<'tcx>>,
    pub predicates: Vec<NumericPredicate<'tcx>>,
}

The set of contract facts known to hold for one graph node.

Fields

contracts: Vec<PropertyContract<'tcx>>

predicates: Vec<NumericPredicate<'tcx>>

Implementations

impl<'tcx> ContractFactSet<'tcx>

pub fn new_default() -> Self

Create an empty contract fact set.

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

Add one contract assumption to the fact set.

pub fn add_predicate(&mut self, predicate: NumericPredicate<'tcx>)

Add one numeric predicate to the fact set.

pub fn get_contracts_length(&self) -> usize

Return the number of contract entries stored in the fact set.

Trait Implementations

impl<'tcx> Clone for ContractFactSet<'tcx>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx> Debug for ContractFactSet<'tcx>

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

Formats the value using the given formatter.