klee
Functions
main.cpp File Reference
#include "klee/Config/Version.h"
#include "klee/Expr/Constraints.h"
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprBuilder.h"
#include "klee/Expr/ExprPPrinter.h"
#include "klee/Expr/ExprSMTLIBPrinter.h"
#include "klee/Expr/ExprVisitor.h"
#include "klee/Expr/Parser/Lexer.h"
#include "klee/Expr/Parser/Parser.h"
#include "klee/Solver/Common.h"
#include "klee/Support/OptionCategories.h"
#include "klee/Statistics/Statistics.h"
#include "klee/Solver/Solver.h"
#include "klee/Solver/SolverCmdLine.h"
#include "klee/Solver/SolverImpl.h"
#include "klee/Support/PrintVersion.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/ManagedStatic.h"
#include "llvm/Support/MemoryBuffer.h"
#include "llvm/Support/raw_ostream.h"
#include <sys/stat.h>
#include <unistd.h>
#include "llvm/Support/Signals.h"
Include dependency graph for main.cpp:

Go to the source code of this file.

Functions

static std::string getQueryLogPath (const char filename[])
 
static std::string escapedString (const char *start, unsigned length)
 
static void PrintInputTokens (const MemoryBuffer *MB)
 
static bool PrintInputAST (const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
 
static bool EvaluateInputAST (const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
 
static bool printInputAsSMTLIBv2 (const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder)
 
int main (int argc, char **argv)
 

Function Documentation

◆ escapedString()

static std::string escapedString ( const char *  start,
unsigned  length 
)
static

Definition at line 122 of file main.cpp.

Referenced by PrintInputTokens().

Here is the caller graph for this function:

◆ EvaluateInputAST()

static bool EvaluateInputAST ( const char *  Filename,
const MemoryBuffer *  MB,
ExprBuilder *  Builder 
)
static

Definition at line 184 of file main.cpp.

References klee::ALL_QUERIES_KQUERY_FILE_NAME, klee::ALL_QUERIES_SMT2_FILE_NAME, klee::constructSolverChain(), klee::CoreSolverToUse, klee::createCoreSolver(), klee::DUMMY_SOLVER, klee::Solver::getInitialValues(), klee::expr::Parser::GetNumErrors(), klee::SolverImpl::getOperationStatusCode(), getQueryLogPath(), klee::StatisticManager::getStatisticByName(), klee::Solver::getValue(), klee::Solver::impl, klee::MaxCoreSolverTime, klee::Solver::mustBeTrue(), klee::expr::Parser::ParseTopLevelDecl(), klee::stats::queries, klee::Solver::setCoreSolverTimeout(), klee::expr::Parser::SetMaxErrors(), klee::SOLVER_QUERIES_KQUERY_FILE_NAME, klee::SOLVER_QUERIES_SMT2_FILE_NAME, and klee::theStatisticManager.

Referenced by main().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getQueryLogPath()

static std::string getQueryLogPath ( const char  filename[])
static

Definition at line 92 of file main.cpp.

Referenced by EvaluateInputAST().

Here is the caller graph for this function:

◆ main()

int main ( int  argc,
char **  argv 
)

Definition at line 387 of file main.cpp.

References klee::createConstantFoldingExprBuilder(), klee::createDefaultExprBuilder(), klee::createSimplifyingExprBuilder(), EvaluateInputAST(), printInputAsSMTLIBv2(), PrintInputAST(), PrintInputTokens(), and klee::printVersion().

Here is the call graph for this function:

◆ printInputAsSMTLIBv2()

static bool printInputAsSMTLIBv2 ( const char *  Filename,
const MemoryBuffer *  MB,
ExprBuilder *  Builder 
)
static

Definition at line 316 of file main.cpp.

References klee::ExprSMTLIBPrinter::generateOutput(), klee::expr::Parser::GetNumErrors(), klee::expr::Parser::ParseTopLevelDecl(), klee::ExprSMTLIBPrinter::setArrayValuesToGet(), klee::expr::Parser::SetMaxErrors(), klee::ExprSMTLIBPrinter::setOutput(), and klee::ExprSMTLIBPrinter::setQuery().

Referenced by main().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ PrintInputAST()

static bool PrintInputAST ( const char *  Filename,
const MemoryBuffer *  MB,
ExprBuilder *  Builder 
)
static

Definition at line 151 of file main.cpp.

References klee::expr::Parser::GetNumErrors(), klee::expr::Parser::ParseTopLevelDecl(), and klee::expr::Parser::SetMaxErrors().

Referenced by main().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ PrintInputTokens()

static void PrintInputTokens ( const MemoryBuffer *  MB)
static

Definition at line 140 of file main.cpp.

References klee::expr::Token::column, escapedString(), klee::expr::Token::getKindName(), klee::expr::Token::kind, klee::expr::Token::length, klee::expr::Lexer::Lex(), klee::expr::Token::line, and klee::expr::Token::start.

Referenced by main().

Here is the call graph for this function:
Here is the caller graph for this function: