cprover
|
#include <constant_pointer_abstract_object.h>
Public Member Functions | |
constant_pointer_abstract_objectt (const typet &type) | |
constant_pointer_abstract_objectt (const typet &type, bool top, bool bottom) | |
constant_pointer_abstract_objectt (const constant_pointer_abstract_objectt &old) | |
constant_pointer_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
exprt | to_constant () const override |
To try and find a constant expression for this abstract object. More... | |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override |
Print the value of the pointer. More... | |
abstract_object_pointert | read_dereference (const abstract_environmentt &env, const namespacet &ns) const override |
A helper function to dereference a value from a pointer. More... | |
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 override |
A helper function to evaluate writing to a pointers value. More... | |
void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
![]() | |
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... | |
![]() | |
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 | 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 |
Protected Member Functions | |
abstract_object_pointert | merge (abstract_object_pointert op1) const override |
Set this abstract object to be the result of merging this abstract object. 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 () |
Private Types | |
typedef sharing_ptrt< constant_pointer_abstract_objectt > | constant_pointer_abstract_pointert |
Private Member Functions | |
abstract_object_pointert | merge_constant_pointers (const constant_pointer_abstract_pointert &other) const |
Merges two constant pointers. More... | |
Private Attributes | |
write_stackt | value_stack |
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 |
Definition at line 19 of file constant_pointer_abstract_object.h.
|
private |
Definition at line 23 of file constant_pointer_abstract_object.h.
|
explicit |
type | the type the abstract_object is representing |
Definition at line 19 of file constant_pointer_abstract_object.cpp.
constant_pointer_abstract_objectt::constant_pointer_abstract_objectt | ( | const typet & | type, |
bool | top, | ||
bool | bottom | ||
) |
type | the type the abstract_object is representing |
top | is the abstract_object starting as top |
bottom | is the abstract_object starting as bottom |
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true
Definition at line 26 of file constant_pointer_abstract_object.cpp.
constant_pointer_abstract_objectt::constant_pointer_abstract_objectt | ( | const constant_pointer_abstract_objectt & | old | ) |
old | the abstract object to copy from |
Definition at line 35 of file constant_pointer_abstract_object.cpp.
constant_pointer_abstract_objectt::constant_pointer_abstract_objectt | ( | const exprt & | expr, |
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
expr | the expression to use as the starting pointer for an abstract object |
environment | the environment in which we evaluate expr |
ns | the current namespace |
Definition at line 41 of file constant_pointer_abstract_object.cpp.
|
overridevirtual |
Reimplemented from abstract_pointer_objectt.
Definition at line 222 of file constant_pointer_abstract_object.cpp.
|
overrideprotectedvirtual |
Set this abstract object to be the result of merging this abstract object.
This calls the merge_constant_pointers if we are trying to merge a constant pointer we use the constant pointer constant pointer merge
op1 | the pointer being merged |
Reimplemented from abstract_objectt.
Definition at line 60 of file constant_pointer_abstract_object.cpp.
|
private |
Merges two constant pointers.
If they are pointing at the same value, we merge, otherwise we set to top.
other | the pointer being merged |
Definition at line 76 of file constant_pointer_abstract_object.cpp.
|
override |
Print the value of the pointer.
Either NULL if nullpointer or ptr -> ( output of what the pointer is pointing to).
out | the stream to write to |
ai | the domain in which this object appears given as ai_baset so that the interface is the same across all domains |
ns | the current namespace |
Definition at line 113 of file constant_pointer_abstract_object.cpp.
|
overridevirtual |
A helper function to dereference a value from a pointer.
Providing the pointer can only be pointing at one thing, returns an abstract object representing that thing. If null or top will return top.
env | the environment |
ns | the namespace |
Reimplemented from abstract_pointer_objectt.
Definition at line 156 of file constant_pointer_abstract_object.cpp.
|
overridevirtual |
To try and find a constant expression for this abstract object.
Reimplemented from abstract_objectt.
Definition at line 99 of file constant_pointer_abstract_object.cpp.
|
overridevirtual |
A helper function to evaluate writing to a pointers value.
If the pointer can only be pointing to one element that it overwrites that element (or merges if merging_write) with the new value. If don't know what we are pointing to, we delegate to the parent.
environment | the environment |
ns | the namespace |
stack | the remaining stack |
value | the value to write to the dereferenced pointer |
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 from abstract_pointer_objectt.
Definition at line 174 of file constant_pointer_abstract_object.cpp.
|
private |
Definition at line 140 of file constant_pointer_abstract_object.h.