klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Interpreter Class Referenceabstract

#include <Interpreter.h>

Inheritance diagram for klee::Interpreter:
Collaboration diagram for klee::Interpreter:

Classes

struct  InterpreterOptions
 
struct  ModuleOptions
 

Public Types

enum  LogType { STP, KQUERY, SMTLIB2 }
 

Public Member Functions

virtual ~Interpreter ()
 
virtual const llvm::Module * setModule (llvm::Module *module, const ModuleOptions &opts)=0
 
virtual void setPathWriter (TreeStreamWriter *tsw)=0
 
virtual void setSymbolicPathWriter (TreeStreamWriter *tsw)=0
 
virtual void setReplayOut (const struct KTest *out)=0
 
virtual void setReplayPath (const std::vector< bool > *path)=0
 
virtual void useSeeds (const std::vector< struct KTest * > *seeds)=0
 
virtual void runFunctionAsMain (llvm::Function *f, int argc, char **argv, char **envp)=0
 
virtual void setHaltExecution (bool value)=0
 
virtual void setInhibitForking (bool value)=0
 
virtual unsigned getPathStreamID (const ExecutionState &state)=0
 
virtual unsigned getSymbolicPathStreamID (const ExecutionState &state)=0
 
virtual void getConstraintLog (const ExecutionState &state, std::string &res, LogType logFormat=STP)=0
 
virtual bool getSymbolicSolution (const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)=0
 
virtual void getCoveredLines (const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)=0
 

Static Public Member Functions

static Interpretercreate (const InterpreterOptions &_interpreterOpts, InterpreterHandler *ih)
 

Protected Member Functions

 Interpreter (const InterpreterOptions &_interpreterOpts)
 

Protected Attributes

const InterpreterOptions interpreterOpts
 

Detailed Description

Definition at line 48 of file Interpreter.h.

Member Enumeration Documentation

Enumerator
STP 
KQUERY 
SMTLIB2 

Definition at line 65 of file Interpreter.h.

Constructor & Destructor Documentation

klee::Interpreter::Interpreter ( const InterpreterOptions _interpreterOpts)
inlineprotected

Definition at line 88 of file Interpreter.h.

virtual klee::Interpreter::~Interpreter ( )
inlinevirtual

Definition at line 93 of file Interpreter.h.

Member Function Documentation

Interpreter * Interpreter::create ( const InterpreterOptions _interpreterOpts,
InterpreterHandler ih 
)
static

Definition at line 3573 of file Executor.cpp.

References klee::Executor::Executor().

Here is the call graph for this function:

virtual void klee::Interpreter::getConstraintLog ( const ExecutionState state,
std::string &  res,
LogType  logFormat = STP 
)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual void klee::Interpreter::getCoveredLines ( const ExecutionState state,
std::map< const std::string *, std::set< unsigned > > &  res 
)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual unsigned klee::Interpreter::getPathStreamID ( const ExecutionState state)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual unsigned klee::Interpreter::getSymbolicPathStreamID ( const ExecutionState state)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual bool klee::Interpreter::getSymbolicSolution ( const ExecutionState state,
std::vector< std::pair< std::string, std::vector< unsigned char > > > &  res 
)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual void klee::Interpreter::runFunctionAsMain ( llvm::Function *  f,
int  argc,
char **  argv,
char **  envp 
)
pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

virtual void klee::Interpreter::setHaltExecution ( bool  value)
pure virtual

Implemented in klee::Executor.

Referenced by halt_execution(), and KleeHandler::processTestCase().

Here is the caller graph for this function:

virtual void klee::Interpreter::setInhibitForking ( bool  value)
pure virtual

Implemented in klee::Executor.

Referenced by stop_forking().

Here is the caller graph for this function:

virtual const llvm::Module* klee::Interpreter::setModule ( llvm::Module *  module,
const ModuleOptions opts 
)
pure virtual

Register the module to be executed.

Returns
The final module after it has been optimized, checks inserted, and modified for interpretation.

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

virtual void klee::Interpreter::setPathWriter ( TreeStreamWriter tsw)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::setInterpreter().

Here is the caller graph for this function:

virtual void klee::Interpreter::setReplayOut ( const struct KTest out)
pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

virtual void klee::Interpreter::setReplayPath ( const std::vector< bool > *  path)
pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

virtual void klee::Interpreter::setSymbolicPathWriter ( TreeStreamWriter tsw)
pure virtual

Implemented in klee::Executor.

Referenced by KleeHandler::setInterpreter().

Here is the caller graph for this function:

virtual void klee::Interpreter::useSeeds ( const std::vector< struct KTest * > *  seeds)
pure virtual

Implemented in klee::Executor.

Referenced by main().

Here is the caller graph for this function:

Member Data Documentation

const InterpreterOptions klee::Interpreter::interpreterOpts
protected

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