cprover
|
#include <value_set_fivrns.h>
Classes | |
struct | entryt |
class | object_map_dt |
Public Types | |
typedef irep_idt | idt |
typedef optionalt< mp_integer > | offsett |
Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset . More... | |
typedef reference_counting< object_map_dt > | object_mapt |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
typedef std::unordered_set< unsigned int > | dynamic_object_id_sett |
typedef std::unordered_map< idt, entryt, string_hash > | valuest |
Public Member Functions | |
value_set_fivrnst () | |
void | set_from (const irep_idt &function, unsigned inx) |
void | set_to (const irep_idt &function, unsigned inx) |
bool | offset_is_zero (offsett offset) const |
exprt | to_expr (object_map_dt::const_iterator it) const |
void | set (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_to (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_to (object_mapt &dest, const exprt &src) const |
bool | insert_to (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const |
bool | insert_to (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const |
bool | insert_to (object_mapt &dest, const exprt &expr, const offsett &offset) const |
bool | insert_from (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert_from (object_mapt &dest, const exprt &src) const |
bool | insert_from (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const |
bool | insert_from (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const |
bool | insert_from (object_mapt &dest, const exprt &expr, const offsett &offset) const |
void | get_value_set (const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const |
expr_sett & | get (const idt &identifier, const std::string &suffix) |
void | clear () |
void | add_var (const idt &id) |
void | add_var (const entryt &e) |
entryt & | get_entry (const idt &id, const std::string &suffix) |
entryt & | get_entry (const entryt &e) |
entryt & | get_temporary_entry (const idt &id, const std::string &suffix) |
void | add_vars (const std::list< entryt > &vars) |
void | output (const namespacet &ns, std::ostream &out) const |
void | output_entry (const entryt &e, const namespacet &ns, std::ostream &out) const |
bool | make_union (object_mapt &dest, const object_mapt &src) const |
bool | make_valid_union (object_mapt &dest, const object_mapt &src) const |
void | copy_objects (object_mapt &dest, const object_mapt &src) const |
void | apply_code (const codet &code, const namespacet &ns) |
bool | handover () |
void | assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false) |
void | do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns) |
void | do_end_function (const exprt &lhs, const namespacet &ns) |
void | get_reference_set (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const |
Public Attributes | |
unsigned | to_function |
unsigned | from_function |
unsigned | to_target_index |
unsigned | from_target_index |
valuest | values |
valuest | temporary_values |
Static Public Attributes | |
static object_numberingt | object_numbering |
static hash_numbering< irep_idt, irep_id_hash > | function_numbering |
Protected Member Functions | |
void | get_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const |
void | get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | get_reference_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | get_reference_set_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
void | dereference_rec (const exprt &src, exprt &dest) const |
void | assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets) |
Definition at line 30 of file value_set_fivrns.h.
typedef std::unordered_set<unsigned int> value_set_fivrnst::dynamic_object_id_sett |
Definition at line 222 of file value_set_fivrns.h.
typedef std::unordered_set<exprt, irep_hash> value_set_fivrnst::expr_sett |
Definition at line 220 of file value_set_fivrns.h.
typedef irep_idt value_set_fivrnst::idt |
Definition at line 54 of file value_set_fivrns.h.
Definition at line 139 of file value_set_fivrns.h.
Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset
.
Definition at line 58 of file value_set_fivrns.h.
typedef std::unordered_map<idt, entryt, string_hash> value_set_fivrnst::valuest |
Definition at line 227 of file value_set_fivrns.h.
|
inline |
Definition at line 33 of file value_set_fivrns.h.
|
inline |
Definition at line 249 of file value_set_fivrns.h.
|
inline |
Definition at line 244 of file value_set_fivrns.h.
|
inline |
Definition at line 275 of file value_set_fivrns.h.
void value_set_fivrnst::apply_code | ( | const codet & | code, |
const namespacet & | ns | ||
) |
void value_set_fivrnst::assign | ( | const exprt & | lhs, |
const exprt & | rhs, | ||
const namespacet & | ns, | ||
bool | add_to_sets = false |
||
) |
|
protected |
|
inline |
Definition at line 239 of file value_set_fivrns.h.
void value_set_fivrnst::copy_objects | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
void value_set_fivrnst::do_end_function | ( | const exprt & | lhs, |
const namespacet & | ns | ||
) |
void value_set_fivrnst::do_function_call | ( | const irep_idt & | function, |
const exprt::operandst & | arguments, | ||
const namespacet & | ns | ||
) |
Definition at line 259 of file value_set_fivrns.h.
Definition at line 254 of file value_set_fivrns.h.
void value_set_fivrnst::get_reference_set | ( | const exprt & | expr, |
expr_sett & | expr_set, | ||
const namespacet & | ns | ||
) | const |
|
inlineprotected |
Definition at line 347 of file value_set_fivrns.h.
|
protected |
|
inline |
Definition at line 269 of file value_set_fivrns.h.
|
protected |
void value_set_fivrnst::get_value_set | ( | const exprt & | expr, |
std::list< exprt > & | expr_set, | ||
const namespacet & | ns | ||
) | const |
|
protected |
bool value_set_fivrnst::handover | ( | ) |
|
inline |
Definition at line 200 of file value_set_fivrns.h.
|
inline |
Definition at line 180 of file value_set_fivrns.h.
|
inline |
Definition at line 185 of file value_set_fivrns.h.
|
inline |
Definition at line 175 of file value_set_fivrns.h.
bool value_set_fivrnst::insert_from | ( | object_mapt & | dest, |
object_numberingt::number_type | n, | ||
const offsett & | offset | ||
) | const |
|
inline |
Definition at line 170 of file value_set_fivrns.h.
|
inline |
Definition at line 151 of file value_set_fivrns.h.
|
inline |
Definition at line 156 of file value_set_fivrns.h.
|
inline |
Definition at line 146 of file value_set_fivrns.h.
bool value_set_fivrnst::insert_to | ( | object_mapt & | dest, |
object_numberingt::number_type | n, | ||
const offsett & | offset | ||
) | const |
bool value_set_fivrnst::make_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
bool value_set_fivrnst::make_valid_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
|
inline |
Definition at line 59 of file value_set_fivrns.h.
void value_set_fivrnst::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
void value_set_fivrnst::output_entry | ( | const entryt & | e, |
const namespacet & | ns, | ||
std::ostream & | out | ||
) | const |
|
inline |
Definition at line 141 of file value_set_fivrns.h.
|
inline |
Definition at line 42 of file value_set_fivrns.h.
|
inline |
Definition at line 48 of file value_set_fivrns.h.
exprt value_set_fivrnst::to_expr | ( | object_map_dt::const_iterator | it | ) | const |
unsigned value_set_fivrnst::from_function |
Definition at line 37 of file value_set_fivrns.h.
unsigned value_set_fivrnst::from_target_index |
Definition at line 38 of file value_set_fivrns.h.
|
static |
Definition at line 40 of file value_set_fivrns.h.
|
static |
Definition at line 39 of file value_set_fivrns.h.
valuest value_set_fivrnst::temporary_values |
Definition at line 294 of file value_set_fivrns.h.
unsigned value_set_fivrnst::to_function |
Definition at line 37 of file value_set_fivrns.h.
unsigned value_set_fivrnst::to_target_index |
Definition at line 38 of file value_set_fivrns.h.
valuest value_set_fivrnst::values |
Definition at line 293 of file value_set_fivrns.h.