cprover
|
#include <value_set_pointer_abstract_object.h>
Public Member Functions | |
value_set_pointer_abstract_objectt (const typet &type) | |
value_set_pointer_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... | |
value_set_pointer_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
exprt | to_constant () const override |
Converts to a constant expression if possible. More... | |
const abstract_object_sett & | get_values () const override |
Getter for the set of stored abstract objects. More... | |
void | set_values (const abstract_object_sett &other_values) |
Setter for updating the stored values. More... | |
abstract_object_pointert | read_dereference (const abstract_environmentt &env, const namespacet &ns) const override |
Evaluate reading the pointer's value. More... | |
abstract_object_pointert | write_dereference (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &new_value, bool merging_write) const override |
Evaluate writing to a pointer's value. More... | |
void | output (std::ostream &out, const ai_baset &ai, 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... | |
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 | 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 |
Static Public Attributes | |
static const size_t | max_value_set_size = 10 |
The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top . More... | |
Protected Member Functions | |
CLONE abstract_object_pointert | merge (abstract_object_pointert other) const override |
Merge two sets of constraints by appending to the first one. 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 Member Functions | |
abstract_object_pointert | resolve_new_values (const abstract_object_sett &new_values, const abstract_environmentt &environment) const |
Update the set of stored values to new_values . More... | |
abstract_object_pointert | resolve_values (const abstract_object_sett &new_values) const |
Update the set of stored values to new_values . More... | |
Private Attributes | |
abstract_object_sett | values |
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 18 of file value_set_pointer_abstract_object.h.
|
explicit |
type | the type the abstract_object is representing |
Definition at line 70 of file value_set_pointer_abstract_object.cpp.
value_set_pointer_abstract_objectt::value_set_pointer_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 77 of file value_set_pointer_abstract_object.cpp.
value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt | ( | const exprt & | expr, |
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
Definition at line 87 of file value_set_pointer_abstract_object.cpp.
|
inlineoverridevirtual |
Getter for the set of stored abstract objects.
Implements value_set_tag.
Definition at line 43 of file value_set_pointer_abstract_object.h.
|
overrideprotectedvirtual |
Merge two sets of constraints by appending to the first one.
Reimplemented from abstract_objectt.
Definition at line 175 of file value_set_pointer_abstract_object.cpp.
|
override |
Definition at line 196 of file value_set_pointer_abstract_object.cpp.
|
overridevirtual |
Evaluate reading the pointer's value.
More precise abstractions may override this to provide more precise results.
env | the environment |
ns | the namespace |
Reimplemented from abstract_pointer_objectt.
Definition at line 97 of file value_set_pointer_abstract_object.cpp.
|
private |
Update the set of stored values to new_values
.
Build a new abstract object of the right type if necessary.
new_values | potentially new set of values |
environment | the abstract environment |
new_values
(either 'this' or something new) Definition at line 142 of file value_set_pointer_abstract_object.cpp.
|
private |
Update the set of stored values to new_values
.
Build a new abstract object of the right type if necessary.
new_values | potentially new set of values |
new_values
(either 'this' or something new) Definition at line 150 of file value_set_pointer_abstract_object.cpp.
void value_set_pointer_abstract_objectt::set_values | ( | const abstract_object_sett & | other_values | ) |
Setter for updating the stored values.
other_values | the new (non-empty) set of values |
Definition at line 188 of file value_set_pointer_abstract_object.cpp.
|
inlineoverridevirtual |
Converts to a constant expression if possible.
If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.
Reimplemented from abstract_objectt.
Definition at line 34 of file value_set_pointer_abstract_object.h.
|
overridevirtual |
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 from abstract_pointer_objectt.
Definition at line 118 of file value_set_pointer_abstract_object.cpp.
|
static |
The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top
.
Definition at line 54 of file value_set_pointer_abstract_object.h.
|
private |
Definition at line 96 of file value_set_pointer_abstract_object.h.