pub trait SpecializeByConditional: Sized {
    // Required methods
    fn add_signed_less_equal_bound(
        self,
        bound: &Bitvector
    ) -> Result<Self, Error>;
    fn add_unsigned_less_equal_bound(
        self,
        bound: &Bitvector
    ) -> Result<Self, Error>;
    fn add_signed_greater_equal_bound(
        self,
        bound: &Bitvector
    ) -> Result<Self, Error>;
    fn add_unsigned_greater_equal_bound(
        self,
        bound: &Bitvector
    ) -> Result<Self, Error>;
    fn add_not_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>;
    fn intersect(self, other: &Self) -> Result<Self, Error>;
    fn without_widening_hints(self) -> Self;
}
Expand description

A trait for domains whose values can be restricted by knowing the result of a comparison of it with a known bitvector. The comparison may also be used to add widening hints to the domain.

Note that the value set represented by the domain after the restriction may be an upper bound, i.e. it is possible that the result still contains values not satisfying the restricting comparison.

Required Methods§

source

fn add_signed_less_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>

Return the restriction of self to values satisfying self <= bound with self and bound interpreted as signed integers. Returns an error if no value represented by self can satisfy the comparison.

source

fn add_unsigned_less_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>

Return the restriction of self to values satisfying self <= bound with self and bound interpreted as unsigned integers. Returns an error if no value represented by self can satisfy the comparison.

source

fn add_signed_greater_equal_bound( self, bound: &Bitvector ) -> Result<Self, Error>

Return the restriction of self to values satisfying self >= bound with self and bound interpreted as signed integers. Returns an error if no value represented by self can satisfy the comparison.

source

fn add_unsigned_greater_equal_bound( self, bound: &Bitvector ) -> Result<Self, Error>

Return the restriction of self to values satisfying self >= bound with self and bound interpreted as unsigned integers. Returns an error if no value represented by self can satisfy the comparison.

source

fn add_not_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>

Return the restriction of self to values satisfying self != bound Returns an error if self only represents one value for which self == bound holds.

source

fn intersect(self, other: &Self) -> Result<Self, Error>

Return the intersection of two values or an error if the intersection is empty.

source

fn without_widening_hints(self) -> Self

Remove all widening hints from self. Necessary for cases where several sources have widening hints, but only one source should contribute widening hints to the result.

Object Safety§

This trait is not object safe.

Implementors§