about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-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>