cprover
|
#include <full_struct_abstract_object.h>
Public Types | |
typedef sharing_ptrt< full_struct_abstract_objectt > | constant_struct_pointert |
typedef abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet > | abstract_aggregate_baset |
![]() | |
typedef std::set< goto_programt::const_targett > | locationst |
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_mapt |
Public Member Functions | |
full_struct_abstract_objectt (const full_struct_abstract_objectt &ao) | |
Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is copy-constructed as well to ensure it shares as much data as possible. More... | |
full_struct_abstract_objectt (const typet &type) | |
full_struct_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... | |
full_struct_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
void | output (std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override |
To provide a human readable string to the out representing 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... | |
void | statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
![]() | |
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 |
Protected Member Functions | |
CLONE abstract_object_pointert | read_component (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const override |
A helper function to evaluate the abstract object contained within a struct. 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 component of a struct. More... | |
bool | verify () const override |
Function: full_struct_abstract_objectt::verify. More... | |
abstract_object_pointert | merge (abstract_object_pointert other) const override |
To merge an abstract object into 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 () |
Private Types | |
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_struct_mapt |
Private Member Functions | |
abstract_object_pointert | merge_constant_structs (constant_struct_pointert other) const |
Performs an element wise merge of the map for each struct. More... | |
Private Attributes | |
shared_struct_mapt | map |
Additional Inherited Members | |
![]() | |
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) |
Definition at line 18 of file full_struct_abstract_object.h.
typedef abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet> full_struct_abstract_objectt::abstract_aggregate_baset |
Definition at line 27 of file full_struct_abstract_object.h.
typedef sharing_ptrt<full_struct_abstract_objectt> full_struct_abstract_objectt::constant_struct_pointert |
Definition at line 23 of file full_struct_abstract_object.h.
|
private |
Definition at line 92 of file full_struct_abstract_object.h.
full_struct_abstract_objectt::full_struct_abstract_objectt | ( | const full_struct_abstract_objectt & | ao | ) |
Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is copy-constructed as well to ensure it shares as much data as possible.
Definition at line 23 of file full_struct_abstract_object.cpp.
|
explicit |
type | the type the abstract_object is representing |
Definition at line 29 of file full_struct_abstract_object.cpp.
full_struct_abstract_objectt::full_struct_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.
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 36 of file full_struct_abstract_object.cpp.
full_struct_abstract_objectt::full_struct_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 46 of file full_struct_abstract_object.cpp.
|
overrideprotectedvirtual |
To merge an abstract object into this abstract object.
If the other is also a struct, we perform a constant_structs merge Otherwise we call back to the parent merge.
other | the other object being merged |
Reimplemented from abstract_objectt.
Definition at line 240 of file full_struct_abstract_object.cpp.
|
private |
Performs an element wise merge of the map for each struct.
other | the other object being merged |
Definition at line 255 of file full_struct_abstract_object.cpp.
|
override |
To provide a human readable string to the out representing the current known value about this object.
For this array we print: { .component_name=<output of object for component_name... }
out | the stream to write to |
ai | the abstract interpreter that contains the abstract domain (that contains the object ... ) |
ns | the current namespace |
Definition at line 201 of file full_struct_abstract_object.cpp.
|
overrideprotectedvirtual |
A helper function to evaluate the abstract object contained within a struct.
More precise abstractions may override this to return more precise results.
environment | the abstract environment |
expr | the expression uses to access a specific component |
ns | the current namespace |
Reimplemented from abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.
Definition at line 75 of file full_struct_abstract_object.cpp.
|
overridevirtual |
Implements abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.
Definition at line 315 of file full_struct_abstract_object.cpp.
|
overrideprotectedvirtual |
Function: full_struct_abstract_objectt::verify.
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
Reimplemented from abstract_objectt.
Definition at line 232 of file full_struct_abstract_object.cpp.
|
overridevirtual |
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.
visitor | an instance of a visitor class that will be applied to all sub elements |
Reimplemented from abstract_objectt.
Definition at line 284 of file full_struct_abstract_object.cpp.
|
overrideprotectedvirtual |
A helper function to evaluate writing to a component of a struct.
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 |
expr | the expression uses to access a specific component |
value | the value we are trying to write to the component |
merging_write | whether to over-write or to merge with the current value. In other words is there any certainty that this write will happen. |
Reimplemented from abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.
Definition at line 109 of file full_struct_abstract_object.cpp.
|
private |
Definition at line 93 of file full_struct_abstract_object.h.