variable_sensitivity_object_factory.cpp File Reference

#include "variable_sensitivity_object_factory.h"
#include "full_array_abstract_object.h"
#include "liveness_context.h"
#include "value_set_pointer_abstract_object.h"

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 22 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 15 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

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
configuration	variable sensitivity domain configuration

Returns

An abstract object of the appropriate type.

Definition at line 72 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 37 of file variable_sensitivity_object_factory.cpp.