diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/CommandLine.h | 78 | ||||
| -rw-r--r-- | include/klee/Common.h | 27 |
2 files changed, 48 insertions, 57 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index c8397cf1..39290e7b 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -1,55 +1,31 @@ /* - * FIXME: This is a temporary solution. - * This header groups command line options and associated data that is common - * for klee and kleaver. + * This header groups command line options declarations and associated data + * that is common for klee and kleaver. */ -#ifndef COMMANDLINE_H -#define COMMANDLINE_H +#ifndef KLEE_COMMANDLINE_H +#define KLEE_COMMANDLINE_H #include "llvm/Support/CommandLine.h" -namespace { +namespace klee { -#define ALL_QUERIES_SMT2_FILE_NAME "all-queries.smt2" -#define SOLVER_QUERIES_SMT2_FILE_NAME "solver-queries.smt2" -#define ALL_QUERIES_PC_FILE_NAME "all-queries.pc" -#define SOLVER_QUERIES_PC_FILE_NAME "solver-queries.pc" - -llvm::cl::opt<bool> -UseFastCexSolver("use-fast-cex-solver", - llvm::cl::init(false), - llvm::cl::desc("(default=off)")); +extern llvm::cl::opt<bool> UseFastCexSolver; -llvm::cl::opt<bool> -UseCexCache("use-cex-cache", - llvm::cl::init(true), - llvm::cl::desc("Use counterexample caching (default=on)")); +extern llvm::cl::opt<bool> UseCexCache; -llvm::cl::opt<bool> -UseCache("use-cache", - llvm::cl::init(true), - llvm::cl::desc("Use validity caching (default=on)")); +extern llvm::cl::opt<bool> UseCache; -llvm::cl::opt<bool> -UseIndependentSolver("use-independent-solver", - llvm::cl::init(true), - llvm::cl::desc("Use constraint independence (default=on)")); +extern llvm::cl::opt<bool> UseIndependentSolver; -llvm::cl::opt<int> -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.")); +extern llvm::cl::opt<int> MinQueryTimeToLog; ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType { - ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format - ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format - SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format + ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format + ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format + SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format }; @@ -57,29 +33,17 @@ enum QueryLoggingSolverType * if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone * wants to patch their copy of LLVM just for these options. */ -llvm::cl::list<QueryLoggingSolverType> 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 .pc (SMT-LIBv2) format"), - clEnumValEnd - ), - llvm::cl::CommaSeparated -); +extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; + +//A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions +template <typename T> +static bool optionIsSet(llvm::cl::list<T> list, T option) +{ + return std::find(list.begin(), list.end(), option) != list.end(); } -namespace klee { - //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions - template <typename T> - static bool optionIsSet(llvm::cl::list<T> list, T option) - { - return std::find(list.begin(), list.end(), option) != list.end(); - } } -#endif /* COMMANDLINE_H */ +#endif /* KLEE_COMMANDLINE_H */ diff --git a/include/klee/Common.h b/include/klee/Common.h new file mode 100644 index 00000000..657b9341 --- /dev/null +++ b/include/klee/Common.h @@ -0,0 +1,27 @@ +//===-- Common.h ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/* + * This file groups declarations that are common to both KLEE and Kleaver. + */ + +#ifndef KLEE_COMMON_H +#define KLEE_COMMON_H + +namespace klee { + +#define ALL_QUERIES_SMT2_FILE_NAME "all-queries.smt2" +#define SOLVER_QUERIES_SMT2_FILE_NAME "solver-queries.smt2" +#define ALL_QUERIES_PC_FILE_NAME "all-queries.pc" +#define SOLVER_QUERIES_PC_FILE_NAME "solver-queries.pc" + +} + +#endif /* KLEE_COMMON_H */ + |