|
| write_location_contextt (const abstract_object_pointert child, const typet &type) |
|
| write_location_contextt (const abstract_object_pointert child, const typet &type, bool top, bool bottom) |
|
| write_location_contextt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
|
virtual | ~write_location_contextt () |
|
bool | has_been_modified (const abstract_object_pointert before) const override |
| Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More...
|
|
abstract_object_pointert | update_location_context (const abstract_objectt::locationst &locations, const bool update_sub_elements) const override |
| Update the location context for an abstract object, potentially propagating the update to any children of this abstract object. More...
|
|
locationst | get_location_union (const locationst &locations) const |
| Construct the union of the location set of the current object, and a the provided location set. More...
|
|
void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override |
| Output a representation of the value of this abstract object. More...
|
|
| context_abstract_objectt (const abstract_object_pointert child, const typet &type) |
|
| context_abstract_objectt (const abstract_object_pointert child, const typet &type, bool top, bool bottom) |
|
| context_abstract_objectt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) |
|
virtual | ~context_abstract_objectt () |
|
const typet & | type () const override |
| Get the real type of the variable this abstract object is representing. More...
|
|
bool | is_top () const override |
| Find out if the abstract object is top. More...
|
|
bool | is_bottom () const override |
| Find out if the abstract object is bottom. More...
|
|
exprt | to_constant () const override |
| Converts to a constant expression if possible. More...
|
|
abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override |
| Try to resolve an expression with the maximum level of precision available. More...
|
|
abstract_object_pointert | unwrap_context () const override |
|
void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
|
abstract_object_pointert | get_child () const |
|
| 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 bool | verify () const |
| Verify the internal structure of an abstract_object is correct. 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...
|
|
abstract_object_pointert | make_top () const |
|
abstract_object_pointert | clear_top () 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 |
|
|
typedef std::set< goto_programt::const_targett > | locationst |
|
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_mapt |
|
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 |
|
CLONE abstract_object_pointert | child_abstract_object |
|
General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt.
Instances of this class are constructed with an abstract_object_pointert, to which most operations are delegated, while at the same time this class handles the tracking of the 'last_written_location' information.
Instances of this class are best constructed via the templated version of this, 'context_abstract_objectt<T>' which provides the same constructors as the standard 'abstract_objectt' class.
Definition at line 34 of file write_location_context.h.
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.
As such, this function gives the ability to perform additional work for a merge.
For the dependency context, this additional work is the tracking of last_written_locations across the merge
- Parameters
-
other | the object to merge with this |
- Returns
- the result of the merge
Reimplemented from abstract_objectt.
Definition at line 167 of file write_location_context.cpp.