ilasynth::CVerifGen Class Reference

#include <genCBMC.hpp>

Public Types
typedef std::map< std::string, CVar * >	CVarMap
typedef std::map< std::string, CFun * >	CFunMap

Public Member Functions
	CVerifGen (const std::string &prefix)
	~CVerifGen ()
CVar *	addInput (const std::string &name, nptr_t node, bool ms=false)
CVar *	addState (const std::string &name, nptr_t node, bool ms=false)
CFun *	addFun (const std::string &name, bool ms=false)
CVar *	addFuncVar (const std::string &name, nptr_t node, bool ms=false)
void	operator() (const Node *n)
void	buildFun (CFun *f, nptr_t nptr)
void	setFunReturn (CFun *f, nptr_t nptr)
void	addFunUpdate (CFun *f, nptr_t lhs, nptr_t rhs)
void	addFunUpdate (CFun *f, nptr_t lhs, CVar *rhs)
void	endFun (CFun *f)
CVar *	appFun (CFun *appFun, CFun *envFun)
void	exportAllToFile (const std::string &fileName) const
void	exportAllToDir (const std::string &dirName) const

Private Member Functions
void	defMemClass (std::ostream &out) const
void	setMemConst (std::ostream &out) const
void	genModel (std::ostream &out) const
void	defUnitpFunc (std::ostream &out) const
void	createCommon (std::ostream &out) const
CVar *	getBoolVarC (const BoolVar *n)
CVar *	getBoolConstC (const BoolConst *n)
CVar *	getBoolOpC (const BoolOp *n)
CVar *	getBvVarC (const BitvectorVar *n)
CVar *	getBvConstC (const BitvectorConst *n)
CVar *	getBvOpC (const BitvectorOp *n)
CVar *	getMemVarC (const MemVar *n)
CVar *	getMemConstC (const MemConst *n)
CVar *	getMemOpC (const MemOp *n)
CVar *	getFuncVarC (const FuncVar *n)
bool	isITE (nptr_t n)
void	depthFirstTraverse (nptr_t n)
std::string	getSignedCCode (CVar *var)
template<class T >
void	checkAndInsert (std::map< std::string, T *> &mp, const std::string &name, T *var, bool force=false)
CVar *	findVar (CVarMap &mp, const std::string &name)

Private Attributes
std::string	_modelName
CVarMap	_states
CVarMap	_inputs
CFunMap	_funMap
CVarMap	_unitpFuncVarMap
CFunMap	_unitpFuncMap
std::map< CVar *, const MemConst * >	_memConst
CVarMap	_masks
std::map< CFun *, CVarMap * >	_varInFun
CFun *	_curFun
CVar *	_curVar
CVarMap *	_curVarMap
CVarMap	_localArray
CVarMap	_localConstVar

Member Typedef Documentation

CFunMap

typedef std::map<std::string, CFun*> ilasynth::CVerifGen::CFunMap

CVarMap

typedef std::map<std::string, CVar*> ilasynth::CVerifGen::CVarMap

Constructor & Destructor Documentation

CVerifGen()

ilasynth::CVerifGen::CVerifGen

(

const std::string &

prefix

)

~CVerifGen()

ilasynth::CVerifGen::~CVerifGen

(

)

Member Function Documentation

addFun()

CFun* ilasynth::CVerifGen::addFun	(	const std::string &	name,
		bool	ms = false
	)

addFuncVar()

CVar* ilasynth::CVerifGen::addFuncVar	(	const std::string &	name,
		nptr_t	node,
		bool	ms = false
	)

addFunUpdate() [1/2]

void ilasynth::CVerifGen::addFunUpdate	(	CFun *	f,
		nptr_t	lhs,
		nptr_t	rhs
	)

addFunUpdate() [2/2]

void ilasynth::CVerifGen::addFunUpdate	(	CFun *	f,
		nptr_t	lhs,
		CVar *	rhs
	)

addInput()

CVar* ilasynth::CVerifGen::addInput	(	const std::string &	name,
		nptr_t	node,
		bool	ms = false
	)

addState()

CVar* ilasynth::CVerifGen::addState	(	const std::string &	name,
		nptr_t	node,
		bool	ms = false
	)

appFun()

CVar* ilasynth::CVerifGen::appFun	(	CFun *	appFun,
		CFun *	envFun
	)

buildFun()

void ilasynth::CVerifGen::buildFun	(	CFun *	f,
		nptr_t	nptr
	)

checkAndInsert()

template<class T >

void ilasynth::CVerifGen::checkAndInsert ( std::map< std::string, T *> &  mp, const std::string &  name, T *  var, bool  force = false  )

private

createCommon()

void ilasynth::CVerifGen::createCommon ( std::ostream &  out ) const

private

defMemClass()

void ilasynth::CVerifGen::defMemClass ( std::ostream &  out ) const

private

defUnitpFunc()

void ilasynth::CVerifGen::defUnitpFunc ( std::ostream &  out ) const

private

depthFirstTraverse()

void ilasynth::CVerifGen::depthFirstTraverse ( nptr_t  n )

private

endFun()

void ilasynth::CVerifGen::endFun

(

CFun *

f

)

exportAllToDir()

void ilasynth::CVerifGen::exportAllToDir

(

const std::string &

dirName

)

const

exportAllToFile()

void ilasynth::CVerifGen::exportAllToFile

(

const std::string &

fileName

)

const

findVar()

CVar* ilasynth::CVerifGen::findVar ( CVarMap &  mp, const std::string &  name  )

private

genModel()

void ilasynth::CVerifGen::genModel ( std::ostream &  out ) const

private

getBoolConstC()

CVar* ilasynth::CVerifGen::getBoolConstC ( const BoolConst *  n )

private

getBoolOpC()

CVar* ilasynth::CVerifGen::getBoolOpC ( const BoolOp *  n )

private

getBoolVarC()

CVar* ilasynth::CVerifGen::getBoolVarC ( const BoolVar *  n )

private

getBvConstC()

CVar* ilasynth::CVerifGen::getBvConstC ( const BitvectorConst *  n )

private

getBvOpC()

CVar* ilasynth::CVerifGen::getBvOpC ( const BitvectorOp *  n )

private

getBvVarC()

CVar* ilasynth::CVerifGen::getBvVarC ( const BitvectorVar *  n )

private

getFuncVarC()

CVar* ilasynth::CVerifGen::getFuncVarC ( const FuncVar *  n )

private

getMemConstC()

CVar* ilasynth::CVerifGen::getMemConstC ( const MemConst *  n )

private

getMemOpC()

CVar* ilasynth::CVerifGen::getMemOpC ( const MemOp *  n )

private

getMemVarC()

CVar* ilasynth::CVerifGen::getMemVarC ( const MemVar *  n )

private

getSignedCCode()

std::string ilasynth::CVerifGen::getSignedCCode ( CVar *  var )

private

isITE()

bool ilasynth::CVerifGen::isITE ( nptr_t  n )

private

operator()()

void ilasynth::CVerifGen::operator()

(

const Node *

n

)

setFunReturn()

void ilasynth::CVerifGen::setFunReturn	(	CFun *	f,
		nptr_t	nptr
	)

setMemConst()

void ilasynth::CVerifGen::setMemConst ( std::ostream &  out ) const

private

Member Data Documentation

_curFun

CFun* ilasynth::CVerifGen::_curFun

private

_curVar

CVar* ilasynth::CVerifGen::_curVar

private

_curVarMap

CVarMap* ilasynth::CVerifGen::_curVarMap

private

_funMap

CFunMap ilasynth::CVerifGen::_funMap

private

_inputs

CVarMap ilasynth::CVerifGen::_inputs

private

_localArray

CVarMap ilasynth::CVerifGen::_localArray

private

_localConstVar

CVarMap ilasynth::CVerifGen::_localConstVar

private

_masks

CVarMap ilasynth::CVerifGen::_masks

private

_memConst

std::map<CVar*, const MemConst*> ilasynth::CVerifGen::_memConst

private

_modelName

std::string ilasynth::CVerifGen::_modelName

private

_states

CVarMap ilasynth::CVerifGen::_states

private

_unitpFuncMap

CFunMap ilasynth::CVerifGen::_unitpFuncMap

private

_unitpFuncVarMap

CVarMap ilasynth::CVerifGen::_unitpFuncVarMap

private

_varInFun

std::map<CFun*, CVarMap*> ilasynth::CVerifGen::_varInFun

private

---

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

• genCBMC.hpp