klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CmdLineOptions.cpp File Reference
#include "klee/CommandLine.h"
Include dependency graph for CmdLineOptions.cpp:

Go to the source code of this file.

Namespaces

 klee
 

Functions

llvm::cl::opt< bool > klee::UseFastCexSolver ("use-fast-cex-solver", llvm::cl::init(false), llvm::cl::desc("(default=off)"))
 
llvm::cl::opt< bool > klee::UseCexCache ("use-cex-cache", llvm::cl::init(true), llvm::cl::desc("Use counterexample caching (default=on)"))
 
llvm::cl::opt< bool > klee::UseCache ("use-cache", llvm::cl::init(true), llvm::cl::desc("Use validity caching (default=on)"))
 
llvm::cl::opt< bool > klee::UseIndependentSolver ("use-independent-solver", llvm::cl::init(true), llvm::cl::desc("Use constraint independence (default=on)"))
 
llvm::cl::opt< bool > klee::DebugValidateSolver ("debug-validate-solver", llvm::cl::init(false))
 
llvm::cl::opt< int > klee::MinQueryTimeToLog ("min-query-time-to-log", llvm::cl::init(0), llvm::cl::value_desc("milliseconds"), llvm::cl::desc("Set time threshold (in ms) for queries logged in files. ""Only queries longer than threshold will be logged. (default=0). ""Set this param to a negative value to log timeouts only."))
 
llvm::cl::opt< double > klee::MaxCoreSolverTime ("max-solver-time", llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), llvm::cl::init(0.0), llvm::cl::value_desc("seconds"))
 
llvm::cl::opt< bool > klee::UseForkedCoreSolver ("use-forked-solver", llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"), llvm::cl::init(true))
 
llvm::cl::opt< bool > klee::CoreSolverOptimizeDivides ("solver-optimize-divides", llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), llvm::cl::init(true))
 
llvm::cl::list
< QueryLoggingSolverType > 
klee::queryLoggingOptions ("use-query-log", llvm::cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."), llvm::cl::values(clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"), clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"), clEnumValEnd), llvm::cl::CommaSeparated)