aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Basic
diff options
context:
space:
mode:
authorJiri Slaby <jirislaby@gmail.com>2017-06-07 13:32:53 +0200
committerDan Liew <delcypher@gmail.com>2017-06-12 17:07:05 +0100
commit6204a1faed8f6ed15318be8da3e8e4b5e2f2a4ac (patch)
treefa1d9d9a149cbfa496f26f133e3b44535e729ace /lib/Basic
parent5289c6135b7baef600257c614ef52f9af10a22e4 (diff)
downloadklee-6204a1faed8f6ed15318be8da3e8e4b5e2f2a4ac.tar.gz
llvm: don't use clEnumValEnd for LLVM 4.0
It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
Diffstat (limited to 'lib/Basic')
-rw-r--r--lib/Basic/CmdLineOptions.cpp18
1 files changed, 9 insertions, 9 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 82cb01b2..54087c21 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -13,6 +13,7 @@
*/
#include "klee/CommandLine.h"
+#include "klee/Config/Version.h"
namespace klee {
@@ -76,9 +77,8 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
clEnumValN(ALL_KQUERY,"all:kquery","All queries in .kquery (KQuery) format"),
clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
clEnumValN(SOLVER_KQUERY,"solver:kquery","All queries reaching the solver in .kquery (KQuery) format"),
- clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"),
- clEnumValEnd
- ),
+ clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format")
+ KLEE_LLVM_CL_VAL_END),
llvm::cl::CommaSeparated
);
@@ -106,8 +106,8 @@ llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
- "Use metaSMT with Boolector"),
- clEnumValEnd),
+ "Use metaSMT with Boolector")
+ KLEE_LLVM_CL_VAL_END),
llvm::cl::init(METASMT_DEFAULT_BACKEND));
#undef METASMT_DEFAULT_BACKEND
@@ -140,8 +140,8 @@ llvm::cl::opt<CoreSolverType> CoreSolverToUse(
llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR),
clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR),
clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
- clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR),
- clEnumValEnd),
+ clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)
+ KLEE_LLVM_CL_VAL_END),
llvm::cl::init(DEFAULT_CORE_SOLVER));
llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
@@ -153,8 +153,8 @@ llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
clEnumValN(Z3_SOLVER, "z3", "Z3"),
clEnumValN(NO_SOLVER, "none",
- "Do not cross check (default)"),
- clEnumValEnd),
+ "Do not cross check (default)")
+ KLEE_LLVM_CL_VAL_END),
llvm::cl::init(NO_SOLVER));
}
#undef STP_IS_DEFAULT_STR