12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H 13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_H 72 void set(
object_mapt &dest, object_map_dt::const_iterator it)
const 74 dest.
write()[it->first]=it->second;
79 return insert(dest, it->first, it->second);
112 entryt(
const idt &_identifier,
const std::string &_suffix):
124 typedef std::map<idt, entryt>
valuest;
126 typedef std::unordered_map<idt, entryt, string_hash>
valuest;
135 const idt &identifier,
136 const std::string &suffix);
149 const entryt &e,
const typet &type,
154 std::ostream &out)
const;
208 const std::string &suffix,
209 const typet &original_type,
216 bool is_simplified)
const;
238 const std::string &suffix,
252 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H The type of an expression.
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
objectt(const mp_integer &_offset)
entryt(const idt &_identifier, const std::string &_suffix)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
bool make_union(object_mapt &dest, const object_mapt &src) const
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool offset_is_zero() const
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
static const object_map_dt blank
static object_numberingt object_numbering
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)
exprt to_expr(object_map_dt::const_iterator it) const
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
std::set< exprt > expr_sett
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
bool insert(object_mapt &dest, const exprt &src) const
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset) const
std::vector< exprt > operandst
std::unordered_map< idt, entryt, string_hash > valuest
entryt & get_entry(const entryt &e, const typet &type, const namespacet &)
void do_end_function(const exprt &lhs, const namespacet &ns)
bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Base class for all expressions.
std::set< unsigned int > dynamic_object_id_sett
bool make_union(const value_sett &new_values)
void output(const namespacet &ns, std::ostream &out) const
A statement in a programming language.
void guard(const exprt &expr, const namespacet &ns)
void do_free(const exprt &op, const namespacet &ns)
number_type number(const T &a)
std::list< exprt > valuest
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void apply_code(const codet &code, const namespacet &ns)
reference_counting< object_map_dt > object_mapt
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)