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§
sourcefn add_signed_less_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>
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.
sourcefn add_unsigned_less_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>
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.
sourcefn add_signed_greater_equal_bound(
self,
bound: &Bitvector
) -> Result<Self, Error>
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.
sourcefn add_unsigned_greater_equal_bound(
self,
bound: &Bitvector
) -> Result<Self, Error>
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.
sourcefn add_not_equal_bound(self, bound: &Bitvector) -> Result<Self, Error>
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.
sourcefn intersect(self, other: &Self) -> Result<Self, Error>
fn intersect(self, other: &Self) -> Result<Self, Error>
Return the intersection of two values or an error if the intersection is empty.
sourcefn without_widening_hints(self) -> Self
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.