|
cprover
|
#include <variable_sensitivity_object_factory.h>
Public Member Functions | |
| variable_sensitivity_object_factoryt (const vsd_configt &options) | |
| abstract_object_pointert | get_abstract_object (const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const |
| Get the appropriate abstract object for the variable under consideration. | |
| abstract_object_pointert | wrap_with_context (const abstract_object_pointert &abstract_object) const |
| variable_sensitivity_object_factoryt ()=delete | |
| variable_sensitivity_object_factoryt (const variable_sensitivity_object_factoryt &)=delete | |
| const vsd_configt & | config () const |
Static Public Member Functions | |
| static variable_sensitivity_object_factory_ptrt | configured_with (const vsd_configt &options) |
Private Member Functions | |
| ABSTRACT_OBJECT_TYPET | get_abstract_object_type (const typet &type) const |
| Decide which abstract object type to use for the variable in question. | |
Private Attributes | |
| vsd_configt | configuration |
| size_t | heap_allocations |
Definition at line 25 of file variable_sensitivity_object_factory.h.
|
inlineexplicit |
Definition at line 34 of file variable_sensitivity_object_factory.h.
|
delete |
|
delete |
|
inline |
Definition at line 68 of file variable_sensitivity_object_factory.h.
|
inlinestatic |
Definition at line 29 of file variable_sensitivity_object_factory.h.
| abstract_object_pointert variable_sensitivity_object_factoryt::get_abstract_object | ( | const typet & | type, |
| bool | top, | ||
| bool | bottom, | ||
| const exprt & | e, | ||
| const abstract_environmentt & | environment, | ||
| const namespacet & | ns ) const |
Get the appropriate abstract object for the variable under consideration.
| type | the type of the variable |
| top | whether the abstract object should be top in the two-value domain |
| bottom | whether the abstract object should be bottom in the two-value domain |
| e | if top and bottom are false this expression is used as the starting pointer for the abstract object |
| environment | the current abstract environment |
| ns | namespace, used when following the input type |
Definition at line 142 of file variable_sensitivity_object_factory.cpp.
|
private |
Decide which abstract object type to use for the variable in question.
| type | the type of the variable the abstract object is meant to represent |
Definition at line 100 of file variable_sensitivity_object_factory.cpp.
| abstract_object_pointert variable_sensitivity_object_factoryt::wrap_with_context | ( | const abstract_object_pointert & | abstract_object | ) | const |
Definition at line 214 of file variable_sensitivity_object_factory.cpp.
|
private |
Definition at line 82 of file variable_sensitivity_object_factory.h.
|
mutableprivate |
Definition at line 83 of file variable_sensitivity_object_factory.h.