CBMC
invariant_sett Member List

This is the complete list of members for invariant_sett, including all inherited members.

add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)invariant_settprotected
add_bounds(unsigned a, const boundst &bound)invariant_settinlineprotected
add_eq(const std::pair< unsigned, unsigned > &eq)invariant_settprotected
add_eq(ineq_sett &dest, const std::pair< unsigned, unsigned > &eq, const std::pair< unsigned, unsigned > &ineq)invariant_settprotected
add_le(const std::pair< unsigned, unsigned > &p)invariant_settinlineprotected
add_ne(const std::pair< unsigned, unsigned > &p)invariant_settinlineprotected
add_type_bounds(const exprt &expr, const typet &type)invariant_settprotected
apply_code(const codet &code)invariant_sett
assignment(const exprt &lhs, const exprt &rhs)invariant_sett
bounds_mapinvariant_sett
bounds_mapt typedefinvariant_sett
boundst typedefinvariant_sett
eq_setinvariant_sett
get_bounds(unsigned a, boundst &dest) constinvariant_settprotected
get_constant(const exprt &expr) constinvariant_settprotected
get_object(const exprt &expr, unsigned &n) constinvariant_settprotected
has_eq(const std::pair< unsigned, unsigned > &p) constinvariant_settinlineprotected
has_le(const std::pair< unsigned, unsigned > &p) constinvariant_settinlineprotected
has_ne(const std::pair< unsigned, unsigned > &p) constinvariant_settinlineprotected
implies(const exprt &expr) constinvariant_sett
implies_rec(const exprt &expr) constinvariant_settprotected
ineq_sett typedefinvariant_sett
intersection(ineq_sett &dest, const ineq_sett &other)invariant_settinlinestatic
invariant_sett(value_setst &_value_sets, inv_object_storet &_object_store, const namespacet &_ns)invariant_settinline
is_eq(std::pair< unsigned, unsigned > p) constinvariant_settprotected
is_falseinvariant_sett
is_ge(std::pair< unsigned, unsigned > p) constinvariant_settinlineprotected
is_gt(std::pair< unsigned, unsigned > p) constinvariant_settinlineprotected
is_le(std::pair< unsigned, unsigned > p) constinvariant_settprotected
is_lt(std::pair< unsigned, unsigned > p) constinvariant_settinlineprotected
is_ne(std::pair< unsigned, unsigned > p) constinvariant_settinlineprotected
le_setinvariant_sett
make_false()invariant_settinline
make_threaded()invariant_settinline
make_true()invariant_settinline
make_union(const invariant_sett &other_invariants)invariant_sett
make_union_bounds_map(const bounds_mapt &other)invariant_settprotected
modifies(const exprt &lhs)invariant_sett
modifies(unsigned a)invariant_settprotected
ne_setinvariant_sett
nnf(exprt &expr, bool negate=false)invariant_settprotectedstatic
nsinvariant_settprotected
object_storeinvariant_settprotected
output(std::ostream &out) constinvariant_sett
remove(ineq_sett &dest, unsigned a)invariant_settinlinestatic
simplify(exprt &expr) constinvariant_sett
strengthen(const exprt &expr)invariant_sett
strengthen_rec(const exprt &expr)invariant_settprotected
threadedinvariant_sett
to_string(unsigned a) constinvariant_settprotected
value_setsinvariant_settprotected