cprover
|
#include <invariant_set.h>
Classes | |
struct | entryt |
Public Member Functions | |
inv_object_storet (const namespacet &_ns) | |
bool | get (const exprt &expr, unsigned &n) |
unsigned | add (const exprt &expr) |
bool | is_constant (unsigned n) const |
bool | is_constant (const exprt &expr) const |
const irep_idt & | operator[] (unsigned n) const |
const exprt & | get_expr (unsigned n) const |
void | output (std::ostream &out) const |
std::string | to_string (unsigned n, const irep_idt &identifier) const |
Static Public Member Functions | |
static bool | is_constant_address (const exprt &expr) |
Protected Types | |
typedef hash_numbering< irep_idt, irep_id_hash > | mapt |
Protected Member Functions | |
std::string | build_string (const exprt &expr) const |
Static Protected Member Functions | |
static bool | is_constant_address_rec (const exprt &expr) |
Protected Attributes | |
const namespacet & | ns |
mapt | map |
std::vector< entryt > | entries |
Definition at line 25 of file invariant_set.h.
|
protected |
Definition at line 61 of file invariant_set.h.
|
inlineexplicit |
Definition at line 28 of file invariant_set.h.
unsigned inv_object_storet::add | ( | const exprt & | expr | ) |
Definition at line 63 of file invariant_set.cpp.
References build_string(), entries, is_constant(), map, and template_numberingt< Map >::number().
Referenced by invariant_propagationt::get_objects().
|
protected |
Definition at line 93 of file invariant_set.cpp.
References from_expr(), irept::get(), symbol_exprt::get_identifier(), irept::get_string(), irept::id(), id2string(), integer2string(), exprt::is_constant(), is_constant_address(), ns, exprt::op0(), exprt::operands(), to_bitvector_type(), to_integer(), to_symbol_expr(), and exprt::type().
bool inv_object_storet::get | ( | const exprt & | expr, |
unsigned & | n | ||
) |
Definition at line 34 of file invariant_set.cpp.
References build_string(), entries, template_numberingt< Map >::get_number(), is_constant(), map, and template_numberingt< Map >::number().
Referenced by invariant_sett::get_object().
|
inline |
Definition at line 46 of file invariant_set.h.
References entries.
Referenced by invariant_sett::get_bounds(), and invariant_sett::get_constant().
bool inv_object_storet::is_constant | ( | unsigned | n | ) | const |
Definition at line 81 of file invariant_set.cpp.
References entries.
Referenced by add(), invariant_sett::add_eq(), and get().
bool inv_object_storet::is_constant | ( | const exprt & | expr | ) | const |
Definition at line 87 of file invariant_set.cpp.
References exprt::is_constant(), and is_constant_address().
|
static |
Definition at line 159 of file invariant_set.cpp.
References irept::id(), is_constant_address_rec(), exprt::op0(), and exprt::operands().
Referenced by build_string(), invariant_sett::get_constant(), and is_constant().
|
staticprotected |
Definition at line 168 of file invariant_set.cpp.
References irept::id(), exprt::is_constant(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by is_constant_address().
|
inline |
Definition at line 41 of file invariant_set.h.
References map.
void inv_object_storet::output | ( | std::ostream & | out | ) | const |
Definition at line 28 of file invariant_set.cpp.
References entries, and to_string().
std::string inv_object_storet::to_string | ( | unsigned | n, |
const irep_idt & | identifier | ||
) | const |
Definition at line 885 of file invariant_set.cpp.
References id2string(), and map.
Referenced by output(), and invariant_sett::to_string().
|
protected |
Definition at line 70 of file invariant_set.h.
Referenced by add(), get(), get_expr(), is_constant(), and output().
|
protected |
Definition at line 62 of file invariant_set.h.
Referenced by add(), get(), operator[](), and to_string().
|
protected |
Definition at line 59 of file invariant_set.h.
Referenced by build_string().