klee
Executor.cpp File Reference
#include "Executor.h"
#include "Context.h"
#include "CoreStats.h"
#include "ExecutionState.h"
#include "ExternalDispatcher.h"
#include "GetElementPtrTypeIterator.h"
#include "ImpliedValue.h"
#include "Memory.h"
#include "MemoryManager.h"
#include "PTree.h"
#include "Searcher.h"
#include "SeedInfo.h"
#include "SpecialFunctionHandler.h"
#include "StatsTracker.h"
#include "TimingSolver.h"
#include "UserSearcher.h"
#include "klee/ADT/KTest.h"
#include "klee/ADT/RNG.h"
#include "klee/Config/Version.h"
#include "klee/Core/Interpreter.h"
#include "klee/Expr/ArrayExprOptimizer.h"
#include "klee/Expr/Assignment.h"
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprPPrinter.h"
#include "klee/Expr/ExprSMTLIBPrinter.h"
#include "klee/Expr/ExprUtil.h"
#include "klee/Module/Cell.h"
#include "klee/Module/InstructionInfoTable.h"
#include "klee/Module/KInstruction.h"
#include "klee/Module/KModule.h"
#include "klee/Solver/Common.h"
#include "klee/Solver/SolverCmdLine.h"
#include "klee/Solver/SolverStats.h"
#include "klee/Statistics/TimerStatIncrementer.h"
#include "klee/Support/Casting.h"
#include "klee/Support/ErrorHandling.h"
#include "klee/Support/FileHandling.h"
#include "klee/Support/FloatEvaluation.h"
#include "klee/Support/ModuleUtil.h"
#include "klee/Support/OptionCategories.h"
#include "klee/System/MemoryUsage.h"
#include "klee/System/Time.h"
#include "llvm/ADT/SmallPtrSet.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/IR/Attributes.h"
#include "llvm/IR/BasicBlock.h"
#include "llvm/IR/Constants.h"
#include "llvm/IR/DataLayout.h"
#include "llvm/IR/Function.h"
#include "llvm/IR/Instructions.h"
#include "llvm/IR/IntrinsicInst.h"
#include "llvm/IR/LLVMContext.h"
#include "llvm/IR/Module.h"
#include "llvm/IR/Operator.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/ErrorHandling.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Path.h"
#include "llvm/Support/Process.h"
#include "llvm/Support/TypeSize.h"
#include "llvm/Support/raw_ostream.h"
#include <algorithm>
#include <cassert>
#include <cerrno>
#include <cstring>
#include <cxxabi.h>
#include <fstream>
#include <iomanip>
#include <iosfwd>
#include <limits>
#include <sstream>
#include <string>
#include <sys/mman.h>
#include <vector>

Go to the source code of this file.

Namespaces

namespace  klee
 

Macros

#define TTYPE(N, I, S)   case StateTerminationType::N: ret = (S); break;
 
#define MARK(N, I)
 

Functions

cl::OptionCategory klee::DebugCat ("Debugging options", "These are debugging options.")
 
cl::OptionCategory klee::ExtCallsCat ("External call policy options", "These options impact external calls.")
 
cl::OptionCategory klee::SeedingCat ("Seeding options", "These options are related to the use of seeds to start exploration.")
 
cl::OptionCategory klee::TerminationCat ("State and overall termination options", "These options control termination of the overall KLEE " "execution and of individual states.")
 
cl::OptionCategory klee::TestGenCat ("Test generation options", "These options impact test generation.")
 
cl::opt< std::string > klee::MaxTime ("max-time", cl::desc("Halt execution after the specified duration. " "Set to 0s to disable (default=0s)"), cl::init("0s"), cl::cat(TerminationCat))
 
void *__dso_handle __attribute__ ((__weak__))
 
static const llvm::fltSemantics * fpWidthToSemantics (unsigned width)
 
static bool shouldWriteTest (const ExecutionState &state)
 
static std::string terminationTypeFileExtension (StateTerminationType type)
 
bool shouldExitOn (StateTerminationType reason)
 
static std::set< std::string > okExternals (okExternalsList, okExternalsList+(sizeof(okExternalsList)/sizeof(okExternalsList[0])))
 

Variables

unsigned dumpStates = 0
 
unsigned dumpPTree = 0
 
static const char * okExternalsList []
 

Macro Definition Documentation

◆ MARK

#define MARK (   N,
 
)

◆ TTYPE

#define TTYPE (   N,
  I,
 
)    case StateTerminationType::N: ret = (S); break;

Function Documentation

◆ __attribute__()

void *__dso_handle __attribute__ ( (__weak__)  )

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

Here is the caller graph for this function:

◆ fpWidthToSemantics()

static const llvm::fltSemantics * fpWidthToSemantics ( unsigned  width)
inlinestatic

Definition at line 1416 of file Executor.cpp.

References klee::Expr::Fl80, klee::Expr::Int32, and klee::Expr::Int64.

Referenced by klee::Executor::executeCall(), and klee::Executor::executeInstruction().

Here is the caller graph for this function:

◆ okExternals()

static std::set< std::string > okExternals ( okExternalsList  ,
okExternalsList sizeof(okExternalsList)/sizeof(okExternalsList[0]) 
)
static

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

Here is the caller graph for this function:

◆ shouldExitOn()

bool shouldExitOn ( StateTerminationType  reason)

Definition at line 3708 of file Executor.cpp.

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

Here is the caller graph for this function:

◆ shouldWriteTest()

static bool shouldWriteTest ( const ExecutionState state)
static

Definition at line 3622 of file Executor.cpp.

References klee::ExecutionState::coveredNew.

Referenced by klee::Executor::terminateStateEarly(), and klee::Executor::terminateStateOnExit().

Here is the caller graph for this function:

◆ terminationTypeFileExtension()

static std::string terminationTypeFileExtension ( StateTerminationType  type)
static

Definition at line 3626 of file Executor.cpp.

References TERMINATION_TYPES.

Referenced by klee::Executor::terminateStateEarly(), klee::Executor::terminateStateOnError(), and klee::Executor::terminateStateOnExit().

Here is the caller graph for this function:

Variable Documentation

◆ dumpPTree

unsigned dumpPTree = 0

Definition at line 433 of file Executor.cpp.

◆ dumpStates

unsigned dumpStates = 0

Definition at line 433 of file Executor.cpp.

◆ okExternalsList

const char* okExternalsList[]
static
Initial value:
= { "printf",
"fprintf",
"puts",
"getpid" }

Definition at line 3773 of file Executor.cpp.