13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
19#include <unordered_set>
61 return offset && offset->is_zero();
70 typedef std::map<object_numberingt::number_type, offsett>
objmapt;
96 std::pair<iterator, bool>
97 insert(
const std::pair<object_numberingt::number_type, offsett> &)
143 dest.write()[it->first]=it->second;
225 typedef std::map<idt, entryt>
valuest;
227 typedef std::unordered_map<idt, entryt, string_hash>
valuest;
232 std::list<exprt> &expr_set,
236 const idt &identifier,
237 const std::string &suffix);
263 std::pair<valuest::iterator, bool>
r=
264 values.insert(std::pair<idt, entryt>(index, e));
266 return r.first->second;
277 for(std::list<entryt>::const_iterator
286 std::ostream &out)
const;
291 std::ostream &out)
const;
338 const std::string &suffix,
367 const std::string &suffix,
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
bool contains(unsigned f, unsigned line) const
validity_ranget(unsigned fnc, unsigned f, unsigned t)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
const_iterator find(object_numberingt::number_type k)
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
objmapt::iterator iterator
std::list< validity_ranget > vrange_listt
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
static const object_map_dt blank
validity_rangest validity_ranges
const_iterator end() const
offsett & operator[](object_numberingt::number_type k)
std::map< unsigned, vrange_listt > validity_rangest
std::map< object_numberingt::number_type, offsett > objmapt
objmapt::const_iterator const_iterator
const_iterator begin() const
static numberingt< irep_idt > function_numbering
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_to(object_mapt &dest, const exprt &src) const
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
std::unordered_set< unsigned int > dynamic_object_id_sett
expr_sett & get(const idt &identifier, const std::string &suffix)
void output(const namespacet &ns, std::ostream &out) const
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
reference_counting< object_map_dt > object_mapt
exprt to_expr(object_map_dt::const_iterator it) const
std::unordered_map< idt, entryt, string_hash > valuest
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
void set_to(const irep_idt &function, unsigned inx)
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
entryt & get_entry(const idt &id, const std::string &suffix)
bool make_union(object_mapt &dest, const object_mapt &src) const
void apply_code(const codet &code, const namespacet &ns)
void do_end_function(const exprt &lhs, const namespacet &ns)
std::unordered_set< exprt, irep_hash > expr_sett
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
void dereference_rec(const exprt &src, exprt &dest) const
void set_from(const irep_idt &function, unsigned inx)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void add_var(const entryt &e)
void add_vars(const std::list< entryt > &vars)
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
entryt & get_entry(const entryt &e)
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
void copy_objects(object_mapt &dest, const object_mapt &src) const
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
void add_var(const idt &id)
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
unsigned from_target_index
void set(object_mapt &dest, object_map_dt::const_iterator it) const
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
bool insert_from(object_mapt &dest, const exprt &src) const
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static object_numberingt object_numbering
bool offset_is_zero(offsett offset) const
const std::string & id2string(const irep_idt &d)
#define UNREACHABLE
This should be used to mark dead code.
entryt(const idt &_identifier, const std::string _suffix)