12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
24 full_array_abstract_objectt,
25 array_aggregate_typet>
112 const std::stack<exprt> &stack,
115 bool merging_write)
const override;
137 bool verify()
const override;
152 const std::stack<exprt> &stack,
155 bool merging_write)
const;
160 const std::stack<exprt> &stack,
163 bool merging_write)
const;
170 bool merging_write)
const;
179 return std::hash<BigInt::ullong_t>{}(i.to_ulong());
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
the current known value about this object.
abstract_object_pointert get_top_entry(const abstract_environmentt &env, const namespacet &ns) const
Short hand method for creating a top element of the array.
abstract_object_pointert write_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
bool verify() const override
To validate that the struct object is in a valid state.
CLONE abstract_object_pointert read_component(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const override
A helper function to read elements from an array.
void set_top_internal() override
Perform any additional structural modifications when setting this object to TOP.
abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a index of an array.
abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const override
Apply a visitor operation to all sub elements of this abstract_object.
abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet > abstract_aggregate_baset
abstract_object_pointert read_element(const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const
abstract_object_pointert write_leaf_element(abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
abstract_object_pointert write_sub_element(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
full_array_abstract_objectt(typet type)
abstract_object_pointert full_array_merge(const full_array_pointert other) const
Merges an array into this array.
sharing_ptrt< full_array_abstract_objectt > const full_array_pointert
sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht > shared_array_mapt
abstract_object_pointert merge(abstract_object_pointert other) const override
Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent m...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A map implemented as a tree where subtrees can be shared between different maps.
The type of an expression, extends irept.
An abstraction of a single value that just stores a constant.
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
size_t operator()(const mp_integer &i) const