klee::KModule Class Reference

#include <KModule.h>

Collaboration diagram for klee::KModule:

[legend]

List of all members.

Public Member Functions
KConstant *	getKConstant (llvm::Constant *c)
	KModule (llvm::Module *_module)
	~KModule ()
void	prepare (const Interpreter::ModuleOptions &opts, InterpreterHandler *ihandler)
	Initialize local data structures.
unsigned	getConstantID (llvm::Constant *c, KInstruction *ki)
	Return an id for the given constant, creating a new one if necessary.
Public Attributes
llvm::Module *	module
llvm::TargetData *	targetData
llvm::Function *	dbgStopPointFn
llvm::Function *	kleeMergeFn
std::vector< KFunction * >	functions
std::map< llvm::Function *, KFunction * >	functionMap
std::set< llvm::Function * >	escapingFunctions
InstructionInfoTable *	infos
std::vector< llvm::Constant * >	constants
std::map< llvm::Constant *, KConstant * >	constantMap
Cell *	constantTable

---

Detailed Description

Definition at line 80 of file KModule.h.

---

Constructor & Destructor Documentation

klee::KModule::KModule

(

llvm::Module *

_module

)

KModule::~KModule

(

)

Definition at line 87 of file KModule.cpp.

References constantTable, functions, infos, module, and targetData.

---

Member Function Documentation

unsigned klee::KModule::getConstantID	(	llvm::Constant *	c,
		KInstruction *	ki
	)

Return an id for the given constant, creating a new one if necessary.

Referenced by klee::KFunction::KFunction().

Here is the caller graph for this function:

KConstant* klee::KModule::getKConstant

(

llvm::Constant *

c

)

void KModule::prepare	(	const Interpreter::ModuleOptions &	opts,
		InterpreterHandler *	ihandler
	)

Initialize local data structures.

Definition at line 193 of file KModule.cpp.

References klee::Interpreter::Interpreter::ModuleOptions::CheckDivZero, dbgStopPointFn, escapingFunctions, forceImport(), klee::KFunction::function, klee::functionEscapes(), functionMap, functions, klee::InstructionInfoTable::getInfo(), klee::KInstruction::info, infos, injectStaticConstructorsAndDestructors(), klee::KInstruction::inst, klee::KFunction::instructions, klee::klee_error(), kleeMergeFn, klee::Interpreter::Interpreter::ModuleOptions::LibraryDir, klee::linkWithLibrary(), module, klee::KFunction::numInstructions, klee::InterpreterHandler::openOutputFile(), llvm::Optimize(), klee::Interpreter::Interpreter::ModuleOptions::Optimize, and targetData.

Referenced by klee::Executor::setModule().

Here is the call graph for this function:

Here is the caller graph for this function:

---

Member Data Documentation

std::map<llvm::Constant*, KConstant*> klee::KModule::constantMap

Definition at line 99 of file KModule.h.

std::vector<llvm::Constant*> klee::KModule::constants

Definition at line 98 of file KModule.h.

Referenced by klee::Executor::bindModuleConstants().

Cell* klee::KModule::constantTable

Definition at line 102 of file KModule.h.

Referenced by klee::Executor::bindModuleConstants(), klee::Executor::eval(), and ~KModule().

llvm::Function* klee::KModule::dbgStopPointFn

Definition at line 86 of file KModule.h.

Referenced by prepare().

std::set<llvm::Function*> klee::KModule::escapingFunctions

Definition at line 94 of file KModule.h.

Referenced by klee::StatsTracker::computeReachableUncovered(), and prepare().

std::map<llvm::Function*, KFunction*> klee::KModule::functionMap

Definition at line 90 of file KModule.h.

Referenced by prepare().

std::vector<KFunction*> klee::KModule::functions

Definition at line 89 of file KModule.h.

Referenced by klee::Executor::bindModuleConstants(), prepare(), klee::StatsTracker::StatsTracker(), and ~KModule().

InstructionInfoTable* klee::KModule::infos

Definition at line 96 of file KModule.h.

Referenced by klee::StatsTracker::computeReachableUncovered(), prepare(), klee::StatsTracker::StatsTracker(), klee::StatsTracker::writeIStats(), and ~KModule().

llvm::Function * klee::KModule::kleeMergeFn

Definition at line 86 of file KModule.h.

Referenced by prepare().

llvm::Module* klee::KModule::module

Definition at line 82 of file KModule.h.

Referenced by klee::SpecialFunctionHandler::bind(), klee::StatsTracker::computeReachableUncovered(), klee::Executor::initializeGlobals(), prepare(), klee::SpecialFunctionHandler::prepare(), klee::StatsTracker::writeIStats(), and ~KModule().

llvm::TargetData* klee::KModule::targetData

Definition at line 83 of file KModule.h.

Referenced by klee::Executor::bindInstructionConstants(), klee::Executor::evalConstantExpr(), klee::Executor::executeInstruction(), klee::Executor::initializeGlobals(), prepare(), and ~KModule().

---

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

• include/klee/Internal/Module/KModule.h
• lib/Module/KModule.cpp