CBMC
|
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_sett | protected |
add_bounds(unsigned a, const boundst &bound) | invariant_sett | inlineprotected |
add_eq(const std::pair< unsigned, unsigned > &eq) | invariant_sett | protected |
add_eq(ineq_sett &dest, const std::pair< unsigned, unsigned > &eq, const std::pair< unsigned, unsigned > &ineq) | invariant_sett | protected |
add_le(const std::pair< unsigned, unsigned > &p) | invariant_sett | inlineprotected |
add_ne(const std::pair< unsigned, unsigned > &p) | invariant_sett | inlineprotected |
add_type_bounds(const exprt &expr, const typet &type) | invariant_sett | protected |
apply_code(const codet &code) | invariant_sett | |
assignment(const exprt &lhs, const exprt &rhs) | invariant_sett | |
bounds_map | invariant_sett | |
bounds_mapt typedef | invariant_sett | |
boundst typedef | invariant_sett | |
eq_set | invariant_sett | |
get_bounds(unsigned a, boundst &dest) const | invariant_sett | protected |
get_constant(const exprt &expr) const | invariant_sett | protected |
get_object(const exprt &expr, unsigned &n) const | invariant_sett | protected |
has_eq(const std::pair< unsigned, unsigned > &p) const | invariant_sett | inlineprotected |
has_le(const std::pair< unsigned, unsigned > &p) const | invariant_sett | inlineprotected |
has_ne(const std::pair< unsigned, unsigned > &p) const | invariant_sett | inlineprotected |
implies(const exprt &expr) const | invariant_sett | |
implies_rec(const exprt &expr) const | invariant_sett | protected |
ineq_sett typedef | invariant_sett | |
intersection(ineq_sett &dest, const ineq_sett &other) | invariant_sett | inlinestatic |
invariant_sett(value_setst &_value_sets, inv_object_storet &_object_store, const namespacet &_ns) | invariant_sett | inline |
is_eq(std::pair< unsigned, unsigned > p) const | invariant_sett | protected |
is_false | invariant_sett | |
is_ge(std::pair< unsigned, unsigned > p) const | invariant_sett | inlineprotected |
is_gt(std::pair< unsigned, unsigned > p) const | invariant_sett | inlineprotected |
is_le(std::pair< unsigned, unsigned > p) const | invariant_sett | protected |
is_lt(std::pair< unsigned, unsigned > p) const | invariant_sett | inlineprotected |
is_ne(std::pair< unsigned, unsigned > p) const | invariant_sett | inlineprotected |
le_set | invariant_sett | |
make_false() | invariant_sett | inline |
make_threaded() | invariant_sett | inline |
make_true() | invariant_sett | inline |
make_union(const invariant_sett &other_invariants) | invariant_sett | |
make_union_bounds_map(const bounds_mapt &other) | invariant_sett | protected |
modifies(const exprt &lhs) | invariant_sett | |
modifies(unsigned a) | invariant_sett | protected |
ne_set | invariant_sett | |
nnf(exprt &expr, bool negate=false) | invariant_sett | protectedstatic |
ns | invariant_sett | protected |
object_store | invariant_sett | protected |
output(std::ostream &out) const | invariant_sett | |
remove(ineq_sett &dest, unsigned a) | invariant_sett | inlinestatic |
simplify(exprt &expr) const | invariant_sett | |
strengthen(const exprt &expr) | invariant_sett | |
strengthen_rec(const exprt &expr) | invariant_sett | protected |
threaded | invariant_sett | |
to_string(unsigned a) const | invariant_sett | protected |
value_sets | invariant_sett | protected |