Go to the documentation of this file.
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> &)
125 return (
function==f &&
from<=line && line<=
to);
143 dest.
write()[it->first]=it->second;
148 return insert_to(dest, it->first, it->second);
213 entryt(
const idt &_identifier,
const std::string _suffix):
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;
317 bool add_to_sets=
false);
338 const std::string &suffix,
339 const typet &original_type,
367 const std::string &suffix,
372 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
#define UNREACHABLE
This should be used to mark dead code.
void get_value_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool contains(unsigned f, unsigned line) const
void set(object_mapt &dest, object_map_dt::const_iterator it) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void output(const namespacet &ns, std::ostream &out) const
exprt to_expr(object_map_dt::const_iterator it) const
const_iterator begin() const
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
The type of an expression, extends irept.
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
std::map< unsigned, vrange_listt > validity_rangest
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void set_to(const irep_idt &function, unsigned inx)
bool insert_from(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
void add_vars(const std::list< entryt > &vars)
std::pair< iterator, bool > insert(const std::pair< object_numberingt::number_type, offsett > &)
std::unordered_set< exprt, irep_hash > expr_sett
unsigned from_target_index
void add_var(const idt &id)
Base class for all expressions.
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
number_type number(const key_type &a)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
bool insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
const std::string & id2string(const irep_idt &d)
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
offsett & operator[](object_numberingt::number_type k)
bool insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
const_iterator end() const
std::list< validity_ranget > vrange_listt
const_iterator find(object_numberingt::number_type k)
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
validity_rangest validity_ranges
std::vector< exprt > operandst
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
reference_counting< object_map_dt > object_mapt
nonstd::optional< T > optionalt
expr_sett & get(const idt &identifier, const std::string &suffix)
void set_from(const irep_idt &function, unsigned inx)
objmapt::const_iterator const_iterator
bool make_union(object_mapt &dest, const object_mapt &src) const
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void copy_objects(object_mapt &dest, const object_mapt &src) const
typename Map::mapped_type number_type
void dereference_rec(const exprt &src, exprt &dest) const
void do_end_function(const exprt &lhs, const namespacet &ns)
bool insert_to(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
bool insert_to(object_mapt &dest, const exprt &src) const
bool insert_to(object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
void add_var(const entryt &e)
entryt & get_entry(const entryt &e)
bool insert_from(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
iterator insert(iterator, const std::pair< object_numberingt::number_type, offsett > &)
bool offset_is_zero(offsett offset) const
static object_numberingt object_numbering
std::map< object_numberingt::number_type, offsett > objmapt
objmapt::iterator iterator
std::unordered_set< unsigned int > dynamic_object_id_sett
static const object_map_dt blank
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
validity_ranget(unsigned fnc, unsigned f, unsigned t)
entryt & get_entry(const idt &id, const std::string &suffix)
bool insert_from(object_mapt &dest, const exprt &src) const
entryt(const idt &_identifier, const std::string _suffix)
void apply_code(const codet &code, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Data structure for representing an arbitrary statement in a program.