Provides an interface for creating and destroying Array objects. More...

#include <ArrayCache.h>

Public Member Functions
	ArrayCache ()

	~ArrayCache ()

const Array *	CreateArray (const std::string &_name, uint64_t _size, const ref< ConstantExpr > constantValuesBegin=0, const ref< ConstantExpr > constantValuesEnd=0, Expr::Width _domain=Expr::Int32, Expr::Width _range=Expr::Int8)
	Create an Array object. More...

Private Types
typedef std::unordered_set< const Array *, klee::ArrayHashFn, klee::EquivArrayCmpFn >	ArrayHashMap

typedef std::vector< const Array * >	ArrayPtrVec

Detailed Description

Provides an interface for creating and destroying Array objects.

Definition at line 31 of file ArrayCache.h.

Member Typedef Documentation

private

Definition at line 65 of file ArrayCache.h.

private

Definition at line 67 of file ArrayCache.h.

klee::ArrayCache::ArrayCache ( )

inline

Definition at line 33 of file ArrayCache.h.

klee::ArrayCache::~ArrayCache ( )

Definition at line 5 of file ArrayCache.cpp.

const Array * klee::ArrayCache::CreateArray	(	const std::string &	_name,
		uint64_t	_size,
		const ref< ConstantExpr > *	constantValuesBegin = `0`,
		const ref< ConstantExpr > *	constantValuesEnd = `0`,
		Expr::Width	_domain = `Expr::Int32`,
		Expr::Width	_range = `Expr::Int8`
	)

Create an Array object.

Symbolic Arrays are cached so that only one instance exists. This provides a limited form of "alpha-renaming". Constant arrays are not cached.

This class retains ownership of Array object so that upon destruction of this object all allocated Array objects are deleted.

Parameters

_name	The name of the array
_size	The size of the array in bytes
constantValuesBegin	A pointer to the beginning of a block of for symbolic arrays.
constantValuesEnd	A pointer +1 pass the end of a block of memory that contains a `ref<ConstantExpr>`. This should be NULL for a symbolic array.
_domain	The size of the domain (i.e. the bitvector used to index the array)
_range	The size of range (i.e. the bitvector that is indexed to)