cprover
|
#include <abstract_pointer_object.h>
Public Member Functions | |
abstract_pointer_objectt (const typet &type) | |
abstract_pointer_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_pointer_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 |
virtual abstract_object_pointert | read_dereference (const abstract_environmentt &env, const namespacet &ns) const |
Evaluate reading the pointer's value. More... | |
virtual abstract_object_pointert | write_dereference (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const |
Evaluate writing to a pointer's value. More... | |
![]() | |
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 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 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 |
Additional Inherited Members | |
![]() | |
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 |
![]() | |
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 (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... | |
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 () |
Definition at line 20 of file abstract_pointer_object.h.
|
explicit |
type | the type the abstract_object is representing |
Definition at line 12 of file abstract_pointer_object.cpp.
abstract_pointer_objectt::abstract_pointer_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.
type | the type the abstract_object is representing |
top | is the abstract_object starting as top |
bottom | is the abstract_object starting as bottom |
Definition at line 18 of file abstract_pointer_object.cpp.
|
explicit |
expr | the expression to use as the starting pointer for an abstract object |
environment | the environment in which the pointer is being created |
ns | the current namespace |
Definition at line 27 of file abstract_pointer_object.cpp.
|
overridevirtual |
Interface for transforms.
expr | the expression to evaluate and find the result of it. This will be the symbol referred to be op0() |
operands | an abstract_object (pointer) that represent the possible values of each operand |
environment | the abstract environment in which the expression is being evaluated |
ns | the current variable namespace |
To try and resolve different expressions with the maximum level of precision available.
Reimplemented from abstract_objectt.
Definition at line 36 of file abstract_pointer_object.cpp.
|
overridevirtual |
Reimplemented from abstract_objectt.
Reimplemented in constant_pointer_abstract_objectt.
Definition at line 86 of file abstract_pointer_object.cpp.
|
virtual |
Evaluate reading the pointer's value.
More precise abstractions may override this to provide more precise results.
env | the environment |
ns | the namespace |
Reimplemented in value_set_pointer_abstract_objectt, and constant_pointer_abstract_objectt.
Definition at line 60 of file abstract_pointer_object.cpp.
|
overridevirtual |
A helper function to evaluate writing to a component of an abstract object.
More precise abstractions may override this to update what they are storing for a specific component.
environment | the abstract environment |
ns | the current namespace |
stack | the remaining stack of expressions on the LHS to evaluate |
specifier | the expression uses to access a specific component |
value | the value we are trying to write to the component |
merging_write | if true, this and all future writes will be merged with the current value |
Reimplemented from abstract_objectt.
Definition at line 49 of file abstract_pointer_object.cpp.
|
virtual |
Evaluate writing to a pointer's value.
More precise abstractions may override this provide more precise results.
environment | the abstract environment |
ns | the namespace |
stack | the remaining stack of expressions on the LHS to evaluate |
value | the value we are trying to assign to what the pointer is pointing to |
merging_write | is it a merging write (i.e. we aren't certain we are writing to this particular pointer therefore the value should be merged with whatever is already there or we are certain we are writing to this pointer so therefore the value can be replaced |
Reimplemented in constant_pointer_abstract_objectt, and value_set_pointer_abstract_objectt.
Definition at line 70 of file abstract_pointer_object.cpp.