CBMC
variable_sensitivity_object_factoryt Class Reference

#include <variable_sensitivity_object_factory.h>

+ Collaboration diagram for variable_sensitivity_object_factoryt:

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. More...
 
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_configtconfig () 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. More...
 

Private Attributes

vsd_configt configuration
 
size_t heap_allocations
 

Detailed Description

Definition at line 25 of file variable_sensitivity_object_factory.h.

Constructor & Destructor Documentation

◆ variable_sensitivity_object_factoryt() [1/3]

variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt ( const vsd_configt options)
inlineexplicit

Definition at line 34 of file variable_sensitivity_object_factory.h.

◆ variable_sensitivity_object_factoryt() [2/3]

variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt ( )
delete

◆ variable_sensitivity_object_factoryt() [3/3]

variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt ( const variable_sensitivity_object_factoryt )
delete

Member Function Documentation

◆ config()

const vsd_configt& variable_sensitivity_object_factoryt::config ( ) const
inline

Definition at line 68 of file variable_sensitivity_object_factory.h.

◆ configured_with()

static variable_sensitivity_object_factory_ptrt variable_sensitivity_object_factoryt::configured_with ( const vsd_configt options)
inlinestatic

Definition at line 29 of file variable_sensitivity_object_factory.h.

◆ get_abstract_object()

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.

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
Returns
An abstract object of the appropriate type.

Definition at line 142 of file variable_sensitivity_object_factory.cpp.

◆ get_abstract_object_type()

ABSTRACT_OBJECT_TYPET variable_sensitivity_object_factoryt::get_abstract_object_type ( const typet type) const
private

Decide which abstract object type to use for the variable in question.

Parameters
typethe type of the variable the abstract object is meant to represent
Returns
An enum indicating the abstract object type to use.

Definition at line 100 of file variable_sensitivity_object_factory.cpp.

◆ wrap_with_context()

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.

Member Data Documentation

◆ configuration

vsd_configt variable_sensitivity_object_factoryt::configuration
private

Definition at line 82 of file variable_sensitivity_object_factory.h.

◆ heap_allocations

size_t variable_sensitivity_object_factoryt::heap_allocations
mutableprivate

Definition at line 83 of file variable_sensitivity_object_factory.h.


The documentation for this class was generated from the following files: