klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::expr::SMTParser Class Reference

#include <SMTParser.h>

Inheritance diagram for klee::expr::SMTParser:
Collaboration diagram for klee::expr::SMTParser:

Public Types

typedef std::map< const
std::string, ExprHandle
VarEnv
 
typedef std::map< const
std::string, ExprHandle
FVarEnv
 

Public Member Functions

 SMTParser (const std::string filename, ExprBuilder *builder)
 
virtual klee::expr::DeclParseTopLevelDecl ()
 
bool Solve ()
 
virtual void SetMaxErrors (unsigned N)
 SetMaxErrors - Suppress anything beyond the first N errors. More...
 
virtual unsigned GetNumErrors () const
 GetNumErrors - Return the number of encountered errors. More...
 
virtual ~SMTParser ()
 
void Parse (void)
 
int Error (const std::string &s)
 
int StringToInt (const std::string &s)
 
ExprHandle GetConstExpr (std::string val, uint8_t base, klee::Expr::Width w)
 
void DeclareExpr (std::string name, Expr::Width w)
 
ExprHandle CreateAnd (std::vector< ExprHandle >)
 
ExprHandle CreateOr (std::vector< ExprHandle >)
 
ExprHandle CreateXor (std::vector< ExprHandle >)
 
void PushVarEnv (void)
 
void PopVarEnv (void)
 
void AddVar (std::string name, ExprHandle val)
 
ExprHandle GetVar (std::string name)
 
void PushFVarEnv (void)
 
void PopFVarEnv (void)
 
void AddFVar (std::string name, ExprHandle val)
 
ExprHandle GetFVar (std::string name)
 
- Public Member Functions inherited from klee::expr::Parser
virtual ~Parser ()
 

Public Attributes

std::string fileName
 
std::istream * is
 
int lineNum
 
bool done
 
bool arraysEnabled
 
std::vector< ExprHandleassumptions
 
klee::expr::ExprHandle satQuery
 
int bvSize
 
bool queryParsed
 
klee::ExprBuilderbuilder
 
std::stack< VarEnvvarEnvs
 
std::stack< FVarEnvfvarEnvs
 

Static Public Attributes

static SMTParserparserTemp = NULL
 

Private Attributes

void * buf
 

Additional Inherited Members

- Static Public Member Functions inherited from klee::expr::Parser
static ParserCreate (const std::string Name, const llvm::MemoryBuffer *MB, ExprBuilder *Builder)
 
- Protected Member Functions inherited from klee::expr::Parser
 Parser ()
 

Detailed Description

Definition at line 25 of file SMTParser.h.

Member Typedef Documentation

typedef std::map<const std::string, ExprHandle> klee::expr::SMTParser::FVarEnv

Definition at line 72 of file SMTParser.h.

typedef std::map<const std::string, ExprHandle> klee::expr::SMTParser::VarEnv

Definition at line 71 of file SMTParser.h.

Constructor & Destructor Documentation

SMTParser::SMTParser ( const std::string  filename,
ExprBuilder builder 
)

Definition at line 37 of file SMTParser.cpp.

References fileName, fvarEnvs, is, and varEnvs.

virtual klee::expr::SMTParser::~SMTParser ( )
inlinevirtual

Definition at line 55 of file SMTParser.h.

Member Function Documentation

void SMTParser::AddFVar ( std::string  name,
ExprHandle  val 
)

Definition at line 231 of file SMTParser.cpp.

References fvarEnvs.

void SMTParser::AddVar ( std::string  name,
ExprHandle  val 
)

Definition at line 203 of file SMTParser.cpp.

References varEnvs.

Referenced by DeclareExpr().

Here is the caller graph for this function:

ExprHandle SMTParser::CreateAnd ( std::vector< ExprHandle kids)

Definition at line 120 of file SMTParser.cpp.

References klee::ExprBuilder::And(), and builder.

Here is the call graph for this function:

ExprHandle SMTParser::CreateOr ( std::vector< ExprHandle kids)

Definition at line 132 of file SMTParser.cpp.

References builder, and klee::ExprBuilder::Or().

Here is the call graph for this function:

ExprHandle SMTParser::CreateXor ( std::vector< ExprHandle kids)

Definition at line 144 of file SMTParser.cpp.

References builder, and klee::ExprBuilder::Xor().

Here is the call graph for this function:

void SMTParser::DeclareExpr ( std::string  name,
Expr::Width  w 
)

Definition at line 157 of file SMTParser.cpp.

References AddVar(), builder, klee::ExprBuilder::Constant(), klee::ConcatExpr::createN(), and klee::ExprBuilder::Read().

Here is the call graph for this function:

int SMTParser::Error ( const std::string &  s)

Definition at line 103 of file SMTParser.cpp.

References fileName, lineNum, and parserTemp.

ExprHandle SMTParser::GetConstExpr ( std::string  val,
uint8_t  base,
klee::Expr::Width  w 
)

Definition at line 181 of file SMTParser.cpp.

References klee::ConstantExpr::alloc().

Here is the call graph for this function:

ExprHandle SMTParser::GetFVar ( std::string  name)

Definition at line 238 of file SMTParser.cpp.

References fvarEnvs.

virtual unsigned klee::expr::SMTParser::GetNumErrors ( ) const
inlinevirtual

GetNumErrors - Return the number of encountered errors.

Implements klee::expr::Parser.

Definition at line 53 of file SMTParser.h.

ExprHandle SMTParser::GetVar ( std::string  name)

Definition at line 210 of file SMTParser.cpp.

References varEnvs.

void SMTParser::Parse ( void  )

Definition at line 52 of file SMTParser.cpp.

References buf, parserTemp, smtlib_bufSize(), smtlib_createBuffer(), smtlib_setInteractive(), smtlib_switchToBuffer(), and smtlibparse().

Referenced by main().

Here is the call graph for this function:

Here is the caller graph for this function:

Decl * SMTParser::ParseTopLevelDecl ( )
virtual

ParseTopLevelDecl - Parse and return a top level declaration, which the caller assumes ownership of.

Returns
NULL indicates the end of the file has been reached.

Implements klee::expr::Parser.

Definition at line 62 of file SMTParser.cpp.

References assumptions, builder, klee::ExprBuilder::Not(), and satQuery.

Referenced by Solve().

Here is the call graph for this function:

Here is the caller graph for this function:

void SMTParser::PopFVarEnv ( void  )

Definition at line 224 of file SMTParser.cpp.

References fvarEnvs.

void SMTParser::PopVarEnv ( void  )

Definition at line 196 of file SMTParser.cpp.

References varEnvs.

void SMTParser::PushFVarEnv ( void  )

Definition at line 220 of file SMTParser.cpp.

References fvarEnvs.

void SMTParser::PushVarEnv ( void  )

Definition at line 189 of file SMTParser.cpp.

References varEnvs.

virtual void klee::expr::SMTParser::SetMaxErrors ( unsigned  N)
inlinevirtual

SetMaxErrors - Suppress anything beyond the first N errors.

Implements klee::expr::Parser.

Definition at line 51 of file SMTParser.h.

bool SMTParser::Solve ( )
int SMTParser::StringToInt ( const std::string &  s)

Definition at line 111 of file SMTParser.cpp.

Member Data Documentation

bool klee::expr::SMTParser::arraysEnabled

Definition at line 36 of file SMTParser.h.

std::vector<ExprHandle> klee::expr::SMTParser::assumptions

Definition at line 38 of file SMTParser.h.

Referenced by ParseTopLevelDecl().

void* klee::expr::SMTParser::buf
private

Definition at line 27 of file SMTParser.h.

Referenced by Parse().

klee::ExprBuilder* klee::expr::SMTParser::builder

Definition at line 44 of file SMTParser.h.

Referenced by CreateAnd(), CreateOr(), CreateXor(), DeclareExpr(), and ParseTopLevelDecl().

int klee::expr::SMTParser::bvSize

Definition at line 41 of file SMTParser.h.

bool klee::expr::SMTParser::done

Definition at line 35 of file SMTParser.h.

std::string klee::expr::SMTParser::fileName

Definition at line 32 of file SMTParser.h.

Referenced by Error(), and SMTParser().

std::stack<FVarEnv> klee::expr::SMTParser::fvarEnvs

Definition at line 75 of file SMTParser.h.

Referenced by AddFVar(), GetFVar(), PopFVarEnv(), PushFVarEnv(), and SMTParser().

std::istream* klee::expr::SMTParser::is

Definition at line 33 of file SMTParser.h.

Referenced by SMTParser().

int klee::expr::SMTParser::lineNum

Definition at line 34 of file SMTParser.h.

Referenced by Error().

SMTParser * SMTParser::parserTemp = NULL
static

Definition at line 31 of file SMTParser.h.

Referenced by Error(), and Parse().

bool klee::expr::SMTParser::queryParsed

Definition at line 42 of file SMTParser.h.

klee::expr::ExprHandle klee::expr::SMTParser::satQuery

Definition at line 39 of file SMTParser.h.

Referenced by ParseTopLevelDecl().

std::stack<VarEnv> klee::expr::SMTParser::varEnvs

Definition at line 74 of file SMTParser.h.

Referenced by AddVar(), GetVar(), PopVarEnv(), PushVarEnv(), and SMTParser().


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