aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorJulian Büning <julian.buening@rwth-aachen.de>2022-01-05 22:43:23 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2022-03-17 22:59:26 +0000
commit1b51cf5ecde7ca9e6646d481b0d757dd31b06da8 (patch)
treeaf3dbec1ca297e4eacc736ba6bb6b012c2a2a8c3
parentfcb5641d29b2e22bbd4034e51a1fe675b69bbf81 (diff)
downloadklee-1b51cf5ecde7ca9e6646d481b0d757dd31b06da8.tar.gz
remove obsolete KLEE_LLVM legacy defines
-rw-r--r--include/klee/Config/Version.h2
-rw-r--r--lib/Core/Executor.cpp8
-rw-r--r--lib/Core/UserSearcher.cpp3
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp3
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp6
-rw-r--r--lib/Module/Checks.cpp4
-rw-r--r--lib/Module/IntrinsicCleaner.cpp3
-rw-r--r--lib/Module/KModule.cpp3
-rw-r--r--lib/Solver/SolverCmdLine.cpp12
-rw-r--r--tools/kleaver/main.cpp6
-rw-r--r--tools/klee/main.cpp2
11 files changed, 18 insertions, 34 deletions
diff --git a/include/klee/Config/Version.h b/include/klee/Config/Version.h
index f3ef8fa5..71cd2d04 100644
--- a/include/klee/Config/Version.h
+++ b/include/klee/Config/Version.h
@@ -14,7 +14,5 @@
#define LLVM_VERSION(major, minor) (((major) << 8) | (minor))
#define LLVM_VERSION_CODE LLVM_VERSION(LLVM_VERSION_MAJOR, LLVM_VERSION_MINOR)
-#define KLEE_LLVM_CL_VAL_END
-#define KLEE_LLVM_GOIF_TERMINATOR
#endif /* KLEE_VERSION_H */
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 682711d3..1a16d389 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -192,8 +192,7 @@ cl::opt<ExternalCallPolicy> ExternalCalls(
"allowed (default)"),
clEnumValN(ExternalCallPolicy::All, "all",
"All external function calls are allowed. This concretizes "
- "any symbolic arguments in calls to external functions.")
- KLEE_LLVM_CL_VAL_END),
+ "any symbolic arguments in calls to external functions.")),
cl::init(ExternalCallPolicy::Concrete),
cl::cat(ExtCallsCat));
@@ -293,8 +292,7 @@ cl::list<StateTerminationType> ExitOnErrorType(
clEnumValN(StateTerminationType::ReportError, "ReportError",
"klee_report_error called"),
clEnumValN(StateTerminationType::User, "User",
- "Wrong klee_* functions invocation")
- KLEE_LLVM_CL_VAL_END),
+ "Wrong klee_* functions invocation")),
cl::ZeroOrMore,
cl::cat(TerminationCat));
@@ -412,7 +410,7 @@ llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions(
"inst_id]"),
clEnumValN(FILE_COMPACT, "compact:file",
"Log all instructions to file instructions.txt in format "
- "[inst_id]") KLEE_LLVM_CL_VAL_END),
+ "[inst_id]")),
llvm::cl::CommaSeparated,
cl::cat(DebugCat));
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index e1534f70..398c44a9 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -47,8 +47,7 @@ cl::list<Searcher::CoreSearchType> CoreSearch(
"use NURS with Instr-Count"),
clEnumValN(Searcher::NURS_CPICnt, "nurs:cpicnt",
"use NURS with CallPath-Instr-Count"),
- clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost")
- KLEE_LLVM_CL_VAL_END),
+ clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost")),
cl::cat(SearchCat));
cl::opt<bool> UseIterativeDeepeningTimeSearch(
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index b329b1ec..0d4707b2 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -38,8 +38,7 @@ llvm::cl::opt<ArrayOptimizationType> OptimizeArray(
clEnumValN(INDEX, "index", "Index-based transformation"),
clEnumValN(VALUE, "value",
"Value-based transformation at branch (both "
- "concrete and concrete/symbolic)")
- KLEE_LLVM_CL_VAL_END),
+ "concrete and concrete/symbolic)")),
llvm::cl::init(NONE),
llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic "
"arrays. (default=false)"),
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 57af2a85..c1bd5822 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -27,8 +27,7 @@ llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode>
clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex",
"Use Hexadecimal form (e.g. #x2D)"),
clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec",
- "Use decimal form (e.g. (_ bv45 8) )")
- KLEE_LLVM_CL_VAL_END),
+ "Use decimal form (e.g. (_ bv45 8) )")),
llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL),
llvm::cl::cat(klee::ExprCat));
@@ -47,8 +46,7 @@ llvm::cl::opt<klee::ExprSMTLIBPrinter::AbbreviationMode> abbreviationMode(
clEnumValN(klee::ExprSMTLIBPrinter::ABBR_LET, "let",
"Abbreviate with let"),
clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NAMED, "named",
- "Abbreviate with :named annotations")
- KLEE_LLVM_CL_VAL_END),
+ "Abbreviate with :named annotations")),
llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET),
llvm::cl::cat(klee::ExprCat));
} // namespace ExprSMTLIBOptions
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 7bb8ec50..1107c2ca 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -73,7 +73,7 @@ bool DivCheckPass::runOnModule(Module &M) {
KleeIRMetaData md(ctx);
auto divZeroCheckFunction =
M.getOrInsertFunction("klee_div_zero_check", Type::getVoidTy(ctx),
- Type::getInt64Ty(ctx) KLEE_LLVM_GOIF_TERMINATOR);
+ Type::getInt64Ty(ctx));
for (auto &divInst : divInstruction) {
llvm::IRBuilder<> Builder(divInst /* Inserts before divInst*/);
@@ -132,7 +132,7 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
KleeIRMetaData md(ctx);
auto overshiftCheckFunction = M.getOrInsertFunction(
"klee_overshift_check", Type::getVoidTy(ctx), Type::getInt64Ty(ctx),
- Type::getInt64Ty(ctx) KLEE_LLVM_GOIF_TERMINATOR);
+ Type::getInt64Ty(ctx));
for (auto &shiftInst : shiftInstructions) {
llvm::IRBuilder<> Builder(shiftInst);
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index d15db10a..7836c202 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -287,8 +287,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
case Intrinsic::trap: {
// Intrinsic instruction "llvm.trap" found. Directly lower it to
// a call of the abort() function.
- auto C = M.getOrInsertFunction("abort", Type::getVoidTy(ctx)
- KLEE_LLVM_GOIF_TERMINATOR);
+ auto C = M.getOrInsertFunction("abort", Type::getVoidTy(ctx));
#if LLVM_VERSION_CODE >= LLVM_VERSION(9, 0)
if (auto *F = dyn_cast<Function>(C.getCallee())) {
#else
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 2f78ce14..06b6e2f9 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -85,8 +85,7 @@ namespace {
clEnumValN(eSwitchTypeLLVM, "llvm",
"lower using LLVM"),
clEnumValN(eSwitchTypeInternal, "internal",
- "execute switch internally")
- KLEE_LLVM_CL_VAL_END),
+ "execute switch internally")),
cl::init(eSwitchTypeInternal),
cl::cat(ModuleCat));
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index 7dd8f041..d91261dc 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -104,8 +104,7 @@ cl::bits<QueryLoggingSolverType> QueryLoggingOptions(
"All queries reaching the solver in .kquery (KQuery) format"),
clEnumValN(
SOLVER_SMTLIB, "solver:smt2",
- "All queries reaching the solver in .smt2 (SMT-LIBv2) format")
- KLEE_LLVM_CL_VAL_END),
+ "All queries reaching the solver in .smt2 (SMT-LIBv2) format")),
cl::CommaSeparated, cl::cat(SolvingCat));
cl::opt<bool> UseAssignmentValidatingSolver(
@@ -158,8 +157,7 @@ MetaSMTBackend("metasmt-backend",
clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
"Use metaSMT with Boolector"),
clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"),
- clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2")
- KLEE_LLVM_CL_VAL_END),
+ clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2")),
cl::init(METASMT_DEFAULT_BACKEND),
cl::cat(SolvingCat));
@@ -195,8 +193,7 @@ cl::opt<CoreSolverType> CoreSolverToUse(
clEnumValN(METASMT_SOLVER, "metasmt",
"metaSMT" METASMT_IS_DEFAULT_STR),
clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
- clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)
- KLEE_LLVM_CL_VAL_END),
+ clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)),
cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat));
cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
@@ -207,8 +204,7 @@ cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
clEnumValN(Z3_SOLVER, "z3", "Z3"),
- clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")
- KLEE_LLVM_CL_VAL_END),
+ clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")),
cl::init(NO_SOLVER), cl::cat(SolvingCat));
} // namespace klee
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 558e7daf..22c23422 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -56,8 +56,7 @@ static llvm::cl::opt<ToolActions> ToolAction(
clEnumValN(PrintAST, "print-ast",
"Print parsed AST nodes from the input file."),
clEnumValN(Evaluate, "evaluate",
- "Evaluate parsed AST nodes from the input file.")
- KLEE_LLVM_CL_VAL_END),
+ "Evaluate parsed AST nodes from the input file.")),
llvm::cl::cat(klee::SolvingCat));
enum BuilderKinds {
@@ -74,8 +73,7 @@ static llvm::cl::opt<BuilderKinds> BuilderKind(
clEnumValN(ConstantFoldingBuilder, "constant-folding",
"Fold constant expressions."),
clEnumValN(SimplifyingBuilder, "simplify",
- "Fold constants and simplify expressions.")
- KLEE_LLVM_CL_VAL_END),
+ "Fold constants and simplify expressions.")),
llvm::cl::cat(klee::ExprCat));
llvm::cl::opt<std::string> DirectoryToWriteQueryLogs(
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 740b33d7..5984c2f9 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -172,7 +172,7 @@ namespace {
"Don't link in a libc (only provide freestanding environment)"),
clEnumValN(LibcType::KleeLibc, "klee", "Link in KLEE's libc"),
clEnumValN(LibcType::UcLibc, "uclibc",
- "Link in uclibc (adapted for KLEE)") KLEE_LLVM_CL_VAL_END),
+ "Link in uclibc (adapted for KLEE)")),
cl::init(LibcType::FreestandingLibc), cl::cat(LinkCat));
cl::list<std::string>