CBMC
variable_sensitivity_object_factory.cpp File Reference
+ Include dependency graph for variable_sensitivity_object_factory.cpp:

Go to the source code of this file.

Functions

template<class context_classt >
abstract_object_pointert create_context_abstract_object (const abstract_object_pointert &abstract_object)
 
template<class abstract_object_classt >
abstract_object_pointert create_abstract_object (const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns)
 
abstract_object_pointert wrap_with_context_object (const abstract_object_pointert &abstract_object, const vsd_configt &configuration)
 
template<class abstract_object_classt >
abstract_object_pointert initialize_abstract_object (const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration)
 Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract object class and return it. More...
 

Function Documentation

◆ create_abstract_object()

template<class abstract_object_classt >
abstract_object_pointert create_abstract_object ( const typet  type,
bool  top,
bool  bottom,
const exprt e,
const abstract_environmentt environment,
const namespacet ns 
)

Definition at line 34 of file variable_sensitivity_object_factory.cpp.

◆ create_context_abstract_object()

template<class context_classt >
abstract_object_pointert create_context_abstract_object ( const abstract_object_pointert abstract_object)

Definition at line 27 of file variable_sensitivity_object_factory.cpp.

◆ initialize_abstract_object()

template<class abstract_object_classt >
abstract_object_pointert initialize_abstract_object ( const typet  type,
bool  top,
bool  bottom,
const exprt e,
const abstract_environmentt environment,
const namespacet ns,
const vsd_configt configuration 
)

Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract object class and return it.

Parameters
typethe type of the variable
topwhether the abstract object should be top in the two-value domain
bottomwhether the abstract object should be bottom in the two-value domain
eif top and bottom are false this expression is used as the starting pointer for the abstract object
environmentthe current abstract environment
nsnamespace, used when following the input type
configurationvariable sensitivity domain configuration
Returns
An abstract object of the appropriate type.

Definition at line 84 of file variable_sensitivity_object_factory.cpp.

◆ wrap_with_context_object()

abstract_object_pointert wrap_with_context_object ( const abstract_object_pointert abstract_object,
const vsd_configt configuration 
)

Definition at line 49 of file variable_sensitivity_object_factory.cpp.