|
| full_array_abstract_objectt (typet type) |
|
| full_array_abstract_objectt (typet type, bool top, bool bottom) |
| Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...
|
|
| full_array_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
|
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override |
| the current known value about this object. More...
|
|
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. More...
|
|
| abstract_aggregate_objectt (const typet &type) |
|
| abstract_aggregate_objectt (const typet &type, bool tp, bool bttm) |
|
| abstract_aggregate_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
|
abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override |
| Interface for transforms. More...
|
|
abstract_object_pointert | write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override |
| A helper function to evaluate writing to a component of an abstract object. More...
|
|
void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
|
| abstract_objectt (const typet &type) |
|
| abstract_objectt (const typet &type, bool top, bool bottom) |
| Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...
|
|
| abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
| Construct an abstract object from the expression. More...
|
|
| abstract_objectt (const typet &type, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
| Ctor for building object of types that differ from the types of input expressions. More...
|
|
virtual | ~abstract_objectt () |
|
virtual const typet & | type () const |
| Get the real type of the variable this abstract object is representing. More...
|
|
virtual bool | is_top () const |
| Find out if the abstract object is top. More...
|
|
virtual bool | is_bottom () const |
| Find out if the abstract object is bottom. More...
|
|
virtual exprt | to_constant () const |
| Converts to a constant expression if possible. More...
|
|
virtual void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const |
| Print the value of the abstract object. More...
|
|
virtual bool | has_been_modified (const abstract_object_pointert before) const |
| Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More...
|
|
virtual abstract_object_pointert | meet (const abstract_object_pointert &other) const |
| Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}. More...
|
|
virtual abstract_object_pointert | update_location_context (const locationst &locations, const bool update_sub_elements) const |
| Update the location context for an abstract object, potentially propogating the update to any children of this abstract object. More...
|
|
abstract_object_pointert | make_top () const |
|
abstract_object_pointert | clear_top () const |
|
virtual abstract_object_pointert | unwrap_context () const |
|
virtual size_t | internal_hash () const |
|
virtual bool | internal_equality (const abstract_object_pointert &other) const |
|
|
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. More...
|
|
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. More...
|
|
void | statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
|
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 merge. More...
|
|
bool | verify () const override |
| To validate that the struct object is in a valid state. More...
|
|
void | set_top_internal () override |
| Perform any additional structural modifications when setting this object to TOP. More...
|
|
virtual internal_abstract_object_pointert | mutable_clone () const |
|
abstract_object_pointert | abstract_object_merge (const abstract_object_pointert other) const |
| Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...
|
|
bool | should_use_base_merge (const abstract_object_pointert other) const |
| To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific. More...
|
|
abstract_object_pointert | abstract_object_meet (const abstract_object_pointert &other) const |
| Helper function for base meet. More...
|
|
bool | should_use_base_meet (const abstract_object_pointert &other) const |
| Helper function to decide if base meet implementation should be used. More...
|
|
void | set_top () |
|
void | set_not_top () |
|
void | set_not_bottom () |
|
|
abstract_object_pointert | read_element (const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const |
|
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 |
|
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 |
|
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 | get_top_entry (const abstract_environmentt &env, const namespacet &ns) const |
| Short hand method for creating a top element of the array. More...
|
|
abstract_object_pointert | full_array_merge (const full_array_pointert other) const |
| Merges an array into this array. More...
|
|
|
static void | dump_map (std::ostream out, const shared_mapt &m) |
|
static void | dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2) |
| Dump all elements in m1 that are different or missing in m2. More...
|
|
static abstract_object_pointert | merge (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications) |
| Clones the first parameter and merges it with the second. More...
|
|
static abstract_object_pointert | merge (abstract_object_pointert op1, abstract_object_pointert op2) |
|
static abstract_object_pointert | meet (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications) |
| Interface method for the meet operation. More...
|
|
template<class T > |
using | internal_sharing_ptrt = std::shared_ptr< T > |
|
typedef internal_sharing_ptrt< class abstract_objectt > | internal_abstract_object_pointert |
|
static bool | merge_shared_maps (const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map) |
|
bool full_array_abstract_objectt::verify |
( |
| ) |
const |
|
overrideprotectedvirtual |
To validate that the struct object is in a valid state.
This means either it is top or bottom, or if neither of those then there exists something in the map of components. If there is something in the map, then it can't be top or bottom
- Returns
- Returns true if the struct is valid
Reimplemented from abstract_objectt.
Definition at line 84 of file full_array_abstract_object.cpp.
Apply a visitor operation to all sub elements of this abstract_object.
A sub element might be a member of a struct, or an element of an array, for instance, but this is entirely determined by the particular derived instance of abstract_objectt.
- Parameters
-
visitor | an instance of a visitor class that will be applied to all sub elements |
- Returns
- A new abstract_object if it's contents is modifed, or this if no modification is needed
Reimplemented from abstract_objectt.
Definition at line 378 of file full_array_abstract_object.cpp.