diff options
| -rw-r--r-- | include/klee/Config/Version.h | 2 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 8 | ||||
| -rw-r--r-- | lib/Core/UserSearcher.cpp | 3 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 3 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 6 | ||||
| -rw-r--r-- | lib/Module/Checks.cpp | 4 | ||||
| -rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 3 | ||||
| -rw-r--r-- | lib/Module/KModule.cpp | 3 | ||||
| -rw-r--r-- | lib/Solver/SolverCmdLine.cpp | 12 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 6 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 2 |
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> |