12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H 13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_H 70 return offset && offset->is_zero();
82 typedef std::map<object_numberingt::number_type, offsett>
data_typet;
122 template <
typename It>
125 template <
typename T>
138 return !(*
this==other);
172 dest.
write()[it.first]=it.second;
183 return insert(dest, it.first, it.second);
247 entryt(
const idt &_identifier,
const std::string &_suffix):
262 return !(*
this==other);
289 typedef std::map<idt, entryt>
valuest;
291 typedef std::unordered_map<idt, entryt, string_hash>
valuest;
306 const idt &identifier,
307 const std::string &suffix);
334 const entryt &e,
const typet &type,
342 std::ostream &out)
const;
467 bool is_simplified)
const;
508 const std::string &suffix,
509 const typet &original_type,
516 const std::string &suffix,
555 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
The type of an expression, extends irept.
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset_value) const
Adds an expression to an object map, with known offset.
number_type number(const key_type &a)
bool offset_is_zero(const offsett &offset) const
Represents a row of a value_sett.
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)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
expr_sett & get(const idt &identifier, const std::string &suffix)
Appears to be unimplemented.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
static const object_map_dt blank
const_iterator end() const
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
const_iterator cend() const
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
std::map< object_numberingt::number_type, offsett > data_typet
offsett & operator[](key_type i)
const_iterator begin() const
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
bool operator!=(const entryt &other) const
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
const entryt * find_entry(const idt &id) const
Finds an entry in this value-set.
const offsett & at(key_type i) const
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
nonstd::optional< T > optionalt
data_typet::value_type value_type
bool operator==(const entryt &other) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
data_typet::const_iterator const_iterator
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
State type in value_set_domaint, used in value-set analysis and goto-symex.
bool insert(object_mapt &dest, const exprt &src) const
Adds an expression to an object map, with unknown offset.
virtual ~value_sett()=default
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
typename Map::mapped_type number_type
bool operator!=(const object_map_dt &other) const
const_iterator cbegin() const
std::vector< exprt > operandst
const_iterator find(T &&t) const
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing entry into an object map.
std::unordered_map< idt, entryt, string_hash > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function's return value to a given LHS expression.
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
Adds an expression and offset to an object map.
void erase(const_iterator it)
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
Base class for all expressions.
void set(object_mapt &dest, const object_map_dt::value_type &it) const
Sets an entry in object map dest to match an existing entry it from a different map.
bool operator==(const object_map_dt &other) const
std::set< unsigned int > dynamic_object_id_sett
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs.
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).
bool make_union(const value_sett &new_values)
Merges an entire existing value_sett's data into this one.
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Data structure for representing an arbitrary statement in a program.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with ....
entryt & get_entry(const entryt &e, const typet &type, const namespacet &ns)
Gets or inserts an entry in this value-set.
data_typet::iterator iterator
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
std::list< exprt > valuest
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See the other overload of get_reference_set.
valuest values
Stores the LHS ID -> RHS expression set map.
void apply_code(const codet &code, const namespacet &ns)
Transforms this value-set by executing a given statement against it.
data_typet::key_type key_type
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
reference_counting< object_map_dt > object_mapt
Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances ca...
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Extracts a member from a struct- or union-typed expression.