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, | |
| I | |||
| ) |
◆ TTYPE
| #define TTYPE | ( | N, | |
| I, | |||
| S | |||
| ) | case StateTerminationType::N: ret = (S); break; |
Function Documentation
◆ __attribute__()
| void *__dso_handle __attribute__ | ( | (__weak__) | ) |
◆ fpWidthToSemantics()
|
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 |
◆ 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 |
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 |
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
|
static |
Initial value:
= { "printf",
"fprintf",
"puts",
"getpid" }
Definition at line 3773 of file Executor.cpp.
