|
| 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 | write_location_context (const locationt &location) const override |
| Update the location context for an abstract object. More...
|
|
abstract_object_pointert | merge_location_context (const locationt &location) const override |
| Update the merge location context for an abstract 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 bool | verify () const |
| Verify the internal structure of an abstract_object is correct. More...
|
|
virtual void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const |
|
virtual abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const |
| Interface for transforms. More...
|
|
virtual exprt | to_constant () const |
| Converts to a constant expression if possible. More...
|
|
exprt | to_predicate (const exprt &name) const |
| Converts to an invariant expression. More...
|
|
virtual 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 |
| A helper function to evaluate writing to a component of an abstract object. 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 | write_location_context (const locationt &location) const |
| Update the write location context for an abstract object. More...
|
|
virtual abstract_object_pointert | merge_location_context (const locationt &location) const |
| Update the merge location context for an abstract object. More...
|
|
abstract_object_pointert | make_top () const |
|
abstract_object_pointert | clear_top () const |
|
virtual abstract_object_pointert | unwrap_context () const |
|
virtual abstract_object_pointert | visit_sub_elements (const abstract_object_visitort &visitor) const |
| Apply a visitor operation to all sub elements of this abstract_object. More...
|
|
virtual size_t | internal_hash () const |
|
virtual bool | internal_equality (const abstract_object_pointert &other) const |
|
virtual exprt | to_predicate_internal (const exprt &name) const |
| to_predicate implementation - derived classes will override More...
|
|
|
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 (const abstract_object_pointert &other, const widen_modet &widen_mode) 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 abstract_object_pointert | read_component (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const |
|
virtual 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 |
|
virtual void | statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const=0 |
|
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...
|
|
virtual abstract_object_pointert | merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const |
| Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. 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 |
|
void | map_put (mp_integer index, const abstract_object_pointert &value, bool overrun) |
|
abstract_object_pointert | map_find_or_top (mp_integer index, const abstract_environmentt &env, const namespacet &ns) 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 widen_modet &widen_mode) const |
| Merges an array into this array. More...
|
|
exprt | to_predicate_internal (const exprt &name) const override |
| to_predicate implementation - derived classes will override 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 combine_result | merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode) |
|
static combine_result | merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode) |
|
static combine_result | meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2) |
| 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, const widen_modet &widen_mode) |
|