cprover
|
#include <value_set_abstract_value.h>
Public Types | |
using | valuest = std::unordered_set< exprt, irep_hash > |
![]() | |
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 | |
value_set_abstract_valuet (const typet &type, bool top=true, bool bottom=false) | |
value_set_abstract_valuet (exprt expr, const abstract_environmentt &environment, const namespacet &ns) | |
value_set_abstract_valuet (const typet &type, valuest values) | |
const valuest & | get_values () const |
Get the possible values for this abstract object. 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 |
Interface for transforms. More... | |
void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override |
Print the value of the 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 | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const |
virtual 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 |
A helper function to evaluate writing to a component of an 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 constexpr CLONE std::size_t | max_value_set_size = 10 |
TODO arbitrary limit, make configurable. More... | |
Protected Member Functions | |
abstract_object_pointert | merge (abstract_object_pointert other) const override |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. 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 Attributes | |
valuest | values |
If BOTTOM then empty. More... | |
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 |
Definition at line 21 of file value_set_abstract_value.h.
using value_set_abstract_valuet::valuest = std::unordered_set<exprt, irep_hash> |
Definition at line 24 of file value_set_abstract_value.h.
|
explicit |
Definition at line 14 of file value_set_abstract_value.cpp.
value_set_abstract_valuet::value_set_abstract_valuet | ( | exprt | expr, |
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
Definition at line 78 of file value_set_abstract_value.cpp.
Definition at line 66 of file value_set_abstract_value.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 191 of file value_set_abstract_value.cpp.
const value_set_abstract_valuet::valuest & value_set_abstract_valuet::get_values | ( | ) | const |
Get the possible values for this abstract object.
Only meaningful when this is neither TOP nor BOTTOM.
Definition at line 23 of file value_set_abstract_value.cpp.
|
overrideprotectedvirtual |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
other | The object to merge with this |
Reimplemented from abstract_objectt.
Definition at line 31 of file value_set_abstract_value.cpp.
|
overridevirtual |
Print the value of the abstract object.
out | the stream to write to |
ai | the abstract interpreter that contains the abstract domain (that contains the object ... ) |
ns | the current namespace |
Reimplemented from abstract_objectt.
Definition at line 98 of file value_set_abstract_value.cpp.
|
overridevirtual |
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 86 of file value_set_abstract_value.cpp.
|
staticconstexpr |
TODO arbitrary limit, make configurable.
Definition at line 43 of file value_set_abstract_value.h.
|
private |
If BOTTOM then empty.
If neither BOTTOM or TOP then the exact set of values. If TOP this field doesn't mean anything and shouldn't be looked at.
Definition at line 63 of file value_set_abstract_value.h.