cprover
|
#include <value_set.h>
Classes | |
struct | entryt |
class | object_map_dt |
class | objectt |
Public Types | |
typedef irep_idt | idt |
typedef reference_counting< object_map_dt > | object_mapt |
typedef std::set< exprt > | expr_sett |
typedef std::set< unsigned int > | dynamic_object_id_sett |
typedef std::unordered_map< idt, entryt, string_hash > | valuest |
Public Member Functions | |
value_sett () | |
exprt | to_expr (object_map_dt::const_iterator it) const |
void | set (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert (object_mapt &dest, object_map_dt::const_iterator it) const |
bool | insert (object_mapt &dest, const exprt &src) const |
bool | insert (object_mapt &dest, const exprt &src, const mp_integer &offset) const |
bool | insert (object_mapt &dest, unsigned n, const objectt &object) const |
bool | insert (object_mapt &dest, const exprt &expr, const objectt &object) const |
void | get_value_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const |
expr_sett & | get (const idt &identifier, const std::string &suffix) |
void | make_any () |
void | clear () |
entryt & | get_entry (const entryt &e, const typet &type, const namespacet &) |
void | output (const namespacet &ns, std::ostream &out) const |
bool | make_union (object_mapt &dest, const object_mapt &src) const |
bool | make_union (const valuest &new_values) |
bool | make_union (const value_sett &new_values) |
void | guard (const exprt &expr, const namespacet &ns) |
void | apply_code (const codet &code, const namespacet &ns) |
void | assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets) |
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, value_setst::valuest &dest, const namespacet &ns) const |
bool | eval_pointer_offset (exprt &expr, const namespacet &ns) const |
Static Public Member Functions | |
static bool | field_sensitive (const irep_idt &id, const typet &type, const namespacet &) |
Public Attributes | |
unsigned | location_number |
valuest | values |
Static Public Attributes | |
static object_numberingt | object_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, bool is_simplified) 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) |
void | do_free (const exprt &op, const namespacet &ns) |
exprt | make_member (const exprt &src, const irep_idt &component_name, const namespacet &ns) |
Definition at line 25 of file value_set.h.
typedef std::set<unsigned int> value_sett::dynamic_object_id_sett |
Definition at line 121 of file value_set.h.
typedef std::set<exprt> value_sett::expr_sett |
Definition at line 119 of file value_set.h.
typedef irep_idt value_sett::idt |
Definition at line 40 of file value_set.h.
Definition at line 70 of file value_set.h.
typedef std::unordered_map<idt, entryt, string_hash> value_sett::valuest |
Definition at line 126 of file value_set.h.
|
inline |
Definition at line 28 of file value_set.h.
void value_sett::apply_code | ( | const codet & | code, |
const namespacet & | ns | ||
) |
Definition at line 1481 of file value_set.cpp.
References assign(), do_free(), namespace_baset::follow(), forall_operands, get_failed_symbol(), codet::get_statement(), guard(), irept::id(), id2string(), irept::is_not_nil(), static_analysis_baset::ns, address_of_exprt::object(), exprt::op0(), exprt::op1(), exprt::operands(), typet::subtype(), to_code(), to_code_assume(), to_symbol_expr(), and exprt::type().
Referenced by value_set_domaint::transform().
void value_sett::assign | ( | const exprt & | lhs, |
const exprt & | rhs, | ||
const namespacet & | ns, | ||
bool | is_simplified, | ||
bool | add_to_sets | ||
) |
Definition at line 1089 of file value_set.cpp.
References assign_rec(), base_type_eq(), struct_union_typet::components(), exprt::copy_to_operands(), namespace_baset::follow(), forall_operands, from_expr(), get_value_set(), irept::id(), index_type(), make_member(), static_analysis_baset::ns, exprt::op0(), exprt::op2(), exprt::operands(), output(), irept::pretty(), member_exprt::set_component_name(), typet::subtype(), to_struct_union_type(), and exprt::type().
Referenced by apply_code(), goto_symex_statet::assignment(), do_end_function(), do_function_call(), guard(), goto_symext::symex_dead(), and goto_symext::symex_decl().
|
protected |
Definition at line 1290 of file value_set.cpp.
References dynamic_object(), namespace_baset::follow(), from_expr(), get_entry(), symbol_exprt::get_identifier(), get_reference_set(), irept::get_string(), irept::id(), irept::id_string(), make_union(), static_analysis_baset::ns, value_sett::entryt::object_map, object_numbering, typecast_exprt::op(), exprt::op0(), exprt::operands(), reference_counting< T >::read(), to_dynamic_object_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
Referenced by assign().
|
inline |
Definition at line 143 of file value_set.h.
References values.
Referenced by value_set_domaint::initialize().
Definition at line 891 of file value_set.cpp.
References irept::id(), exprt::op0(), exprt::operands(), and exprt::type().
void value_sett::do_end_function | ( | const exprt & | lhs, |
const namespacet & | ns | ||
) |
Definition at line 1469 of file value_set.cpp.
References assign(), irept::is_nil(), static_analysis_baset::ns, and exprt::type().
Referenced by value_set_domaint::transform().
|
protected |
Definition at line 1210 of file value_set.cpp.
References dynamic_object(), get_value_set(), irept::id(), insert(), exprt::is_true(), static_analysis_baset::ns, object_numbering, reference_counting< T >::read(), to_dynamic_object_expr(), exprt::type(), dynamic_object_exprt::valid(), and values.
Referenced by apply_code().
void value_sett::do_function_call | ( | const irep_idt & | function, |
const exprt::operandst & | arguments, | ||
const namespacet & | ns | ||
) |
Definition at line 1423 of file value_set.cpp.
References assign(), namespacet::lookup(), static_analysis_baset::ns, code_typet::parameters(), to_code_type(), and symbolt::type.
Referenced by value_set_domaint::transform().
bool value_sett::eval_pointer_offset | ( | exprt & | expr, |
const namespacet & | ns | ||
) | const |
Definition at line 261 of file value_set.cpp.
References compute_pointer_offset(), Forall_operands, from_integer(), get_value_set(), irept::id(), static_analysis_baset::ns, object_numbering, exprt::op0(), exprt::operands(), irept::swap(), and exprt::type().
Referenced by get_value_set_rec().
|
static |
Definition at line 39 of file value_set.cpp.
References namespace_baset::follow(), has_prefix(), irept::id(), id2string(), and static_analysis_baset::ns.
Referenced by get_entry().
value_sett::entryt & value_sett::get_entry | ( | const entryt & | e, |
const typet & | type, | ||
const namespacet & | ns | ||
) |
Definition at line 54 of file value_set.cpp.
References field_sensitive(), id2string(), value_sett::entryt::identifier, static_analysis_baset::ns, r, value_sett::entryt::suffix, and values.
Referenced by assign_rec().
void value_sett::get_reference_set | ( | const exprt & | expr, |
value_setst::valuest & | dest, | ||
const namespacet & | ns | ||
) | const |
Definition at line 909 of file value_set.cpp.
References static_analysis_baset::ns, reference_counting< T >::read(), and to_expr().
Referenced by assign_rec(), value_set_domaint::get_reference_set(), get_reference_set_rec(), and get_value_set_rec().
|
inlineprotected |
Definition at line 218 of file value_set.h.
References get_reference_set_rec().
|
protected |
Definition at line 924 of file value_set.cpp.
References index_exprt::array(), namespace_baset::follow(), from_expr(), from_integer(), irept::get(), get_reference_set(), get_value_set_rec(), irept::id(), irept::id_string(), index_exprt::index(), index_type(), insert(), exprt::is_zero(), exprt::make_typecast(), static_analysis_baset::ns, object_numbering, value_sett::objectt::offset, value_sett::objectt::offset_is_set, value_sett::objectt::offset_is_zero(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_size(), reference_counting< T >::read(), typet::subtype(), to_index_expr(), to_integer(), and exprt::type().
Referenced by get_reference_set().
void value_sett::get_value_set | ( | const exprt & | expr, |
value_setst::valuest & | dest, | ||
const namespacet & | ns | ||
) | const |
Definition at line 314 of file value_set.cpp.
References from_expr(), static_analysis_baset::ns, reference_counting< T >::read(), and to_expr().
Referenced by assign(), do_free(), eval_pointer_offset(), symex_dereference_statet::get_value_set(), and postconditiont::is_used().
|
protected |
Definition at line 335 of file value_set.cpp.
References get_value_set_rec(), static_analysis_baset::ns, simplify(), and exprt::type().
|
protected |
Definition at line 348 of file value_set.cpp.
References char_type(), struct_union_typet::components(), dynamic_object(), eval_pointer_offset(), irept::find(), namespace_baset::follow(), forall_operands, from_expr(), irept::get(), symbol_exprt::get_identifier(), get_reference_set(), irept::get_string(), irept::id(), id2string(), irept::id_string(), insert(), exprt::is_constant(), exprt::is_zero(), location_number, make_union(), member_offset(), static_analysis_baset::ns, object_numbering, value_sett::objectt::offset_is_set, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_size(), reference_counting< T >::read(), simplify(), typet::subtype(), to_dynamic_object_expr(), to_expr(), to_integer(), to_struct_type(), to_struct_union_type(), to_symbol_expr(), to_union_type(), exprt::type(), unsigned_char_type(), values, and reference_counting< T >::write().
Referenced by get_reference_set_rec(), and get_value_set().
void value_sett::guard | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 1616 of file value_set.cpp.
References assign(), dynamic_object(), forall_operands, irept::id(), static_analysis_baset::ns, exprt::op0(), exprt::operands(), exprt::type(), and unsigned_char_type().
Referenced by apply_code(), and value_set_domaint::transform().
|
inline |
Definition at line 77 of file value_set.h.
Referenced by do_free(), get_reference_set_rec(), get_value_set_rec(), insert(), and make_union().
|
inline |
Definition at line 82 of file value_set.h.
References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.
|
inline |
Definition at line 87 of file value_set.h.
References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.
bool value_sett::insert | ( | object_mapt & | dest, |
unsigned | n, | ||
const objectt & | object | ||
) | const |
Definition at line 72 of file value_set.cpp.
References reference_counting< T >::read(), and reference_counting< T >::write().
|
inline |
Definition at line 97 of file value_set.h.
References insert(), hash_numbering< T, hash_fkt >::number(), and object_numbering.
|
inline |
Definition at line 138 of file value_set.h.
References values.
|
protected |
Definition at line 1650 of file value_set.cpp.
References struct_union_typet::component_number(), struct_union_typet::component_type(), namespace_baset::follow(), irept::id(), static_analysis_baset::ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), member_exprt::set_component_name(), to_struct_union_type(), and exprt::type().
Referenced by assign().
bool value_sett::make_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
Definition at line 246 of file value_set.cpp.
References insert(), and reference_counting< T >::read().
Referenced by assign_rec(), get_value_set_rec(), make_union(), value_set_domaint::merge(), and goto_symext::merge_value_sets().
bool value_sett::make_union | ( | const valuest & | new_values | ) |
Definition at line 207 of file value_set.cpp.
References make_union(), value_sett::entryt::object_map, and values.
|
inline |
Definition at line 165 of file value_set.h.
References make_union(), and values.
void value_sett::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Definition at line 97 of file value_set.cpp.
References symbolt::display_name(), from_expr(), from_type(), has_prefix(), irept::id(), id2string(), value_sett::entryt::identifier, integer2string(), irept::is_nil(), namespacet::lookup(), symbolt::name, static_analysis_baset::ns, value_sett::entryt::object_map, object_numbering, reference_counting< T >::read(), value_sett::entryt::suffix, exprt::type(), and values.
Referenced by assign(), goto_symex_statet::assignment(), symex_dereference_statet::get_value_set(), and value_set_domaint::output().
|
inline |
Definition at line 72 of file value_set.h.
References reference_counting< T >::write().
exprt value_sett::to_expr | ( | object_map_dt::const_iterator | it | ) | const |
Definition at line 187 of file value_set.cpp.
References from_integer(), index_type(), object_descriptor_exprt::object(), object_numbering, object_descriptor_exprt::offset(), and exprt::type().
Referenced by get_reference_set(), get_value_set(), and get_value_set_rec().
unsigned value_sett::location_number |
Definition at line 37 of file value_set.h.
Referenced by get_value_set_rec(), and value_set_domaint::initialize().
|
static |
Definition at line 38 of file value_set.h.
Referenced by assign_rec(), do_free(), eval_pointer_offset(), get_reference_set_rec(), get_value_set_rec(), insert(), output(), and to_expr().
valuest value_sett::values |
Definition at line 156 of file value_set.h.
Referenced by clear(), value_set_analysist::convert(), do_free(), get_entry(), get_value_set_rec(), make_any(), make_union(), and output().