13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H
18#include <unordered_set>
60 return offset && offset->is_zero();
69 typedef std::map<object_numberingt::number_type, offsett>
objmapt;
95 std::pair<iterator, bool>
96 insert(
const std::pair<object_numberingt::number_type, offsett> &)
143 dest.write()[it->first]=it->second;
225 typedef std::map<idt, entryt>
valuest;
231 typedef std::unordered_map<idt, entryt, string_hash>
valuest;
240 std::list<exprt> &expr_set,
244 const idt &identifier,
245 const std::string &suffix);
271 std::pair<valuest::iterator, bool>
r=
272 values.insert(std::pair<idt, entryt>(index, e));
274 return r.first->second;
285 for(std::list<entryt>::const_iterator
294 std::ostream &out)
const;
346 const std::string &suffix,
376 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)
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
bool set_valid_at(unsigned inx, const validity_ranget &vr)
const_iterator begin() const
objmapt::const_iterator const_iterator
std::map< unsigned, vrange_listt > validity_rangest
const_iterator find(object_numberingt::number_type k)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
const_iterator end() const
validity_rangest validity_ranges
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
offsett & operator[](object_numberingt::number_type k)
std::map< object_numberingt::number_type, offsett > objmapt
objmapt::iterator iterator
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
static const object_map_dt blank
std::list< validity_ranget > vrange_listt
std::unordered_set< unsigned int > dynamic_object_id_sett
std::unordered_set< idt, string_hash > recfind_recursion_sett
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void flatten(const entryt &e, object_mapt &dest) const
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
void add_var(const entryt &e)
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void dereference_rec(const exprt &src, exprt &dest) const
void get_reference_set_sharing(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
std::unordered_set< idt, string_hash > gvs_recursion_sett
static object_numberingt object_numbering
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
std::unordered_set< idt, string_hash > flatten_seent
expr_sett & get(const idt &identifier, const std::string &suffix)
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
entryt & get_entry(const idt &id, const std::string &suffix)
void do_end_function(const exprt &lhs, const namespacet &ns)
void apply_code(const codet &code, const namespacet &ns)
unsigned from_target_index
void output(const namespacet &ns, std::ostream &out) const
std::unordered_set< exprt, irep_hash > expr_sett
bool offset_is_zero(const offsett &offset) const
bool insert_from(object_mapt &dest, const exprt &src) const
void add_var(const idt &id)
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
entryt & get_entry(const entryt &e)
bool insert_to(object_mapt &dest, const exprt &src) const
std::unordered_set< idt, string_hash > assign_recursion_sett
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
static numberingt< irep_idt > function_numbering
bool make_union(object_mapt &dest, const object_mapt &src) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets)
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void add_vars(const std::list< entryt > &vars)
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
void set_from(const irep_idt &function, unsigned inx)
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function) const
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
reference_counting< object_map_dt > object_mapt
std::unordered_map< idt, entryt, string_hash > valuest
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
void set_to(const irep_idt &function, unsigned inx)
void copy_objects(object_mapt &dest, const object_mapt &src) const
exprt to_expr(object_map_dt::const_iterator it) const
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) 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)