about summary refs log tree commit diff homepage
path: root/lib
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
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')
-rw-r--r--lib/Basic/CmdLineOptions.cpp18
-rw-r--r--lib/Core/Executor.cpp8
-rw-r--r--lib/Core/UserSearcher.cpp4
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp8
-rw-r--r--lib/Module/KModule.cpp4
5 files changed, 21 insertions, 21 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
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 5af31125..fea9781d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -156,8 +156,8 @@ namespace {
                                            "inst_id]"),
           clEnumValN(FILE_COMPACT, "compact:file",
                      "Log all instructions to file instructions.txt in format "
-                     "[inst_id]"),
-          clEnumValEnd),
+                     "[inst_id]")
+          KLEE_LLVM_CL_VAL_END),
       llvm::cl::CommaSeparated);
 #ifdef HAVE_ZLIB_H
   cl::opt<bool> DebugCompressInstructions(
@@ -288,8 +288,8 @@ namespace {
 		    clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"),
 		    clEnumValN(Executor::ReportError, "ReportError", "klee_report_error called"),
 		    clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
-		    clEnumValN(Executor::Unhandled, "Unhandled", "Unhandled instruction hit"),
-		    clEnumValEnd),
+		    clEnumValN(Executor::Unhandled, "Unhandled", "Unhandled instruction hit")
+		    KLEE_LLVM_CL_VAL_END),
 		  cl::ZeroOrMore);
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0)
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 725836e8..2bbbe747 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -30,8 +30,8 @@ namespace {
 			clEnumValN(Searcher::NURS_Depth, "nurs:depth", "use NURS with 2^depth"),
 			clEnumValN(Searcher::NURS_ICnt, "nurs:icnt", "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"),
-			clEnumValEnd));
+			clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost")
+			KLEE_LLVM_CL_VAL_END));
 
   cl::opt<bool>
   UseIterativeDeepeningTimeSearch("use-iterative-deepening-time-search", 
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index e8e9a253..192e3461 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -25,8 +25,8 @@ argConstantDisplayMode(
                      clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex",
                                 "Use Hexadecimal form (e.g. #x2D)"),
                      clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec",
-                                "Use decimal form (e.g. (_ bv45 8) )"),
-                     clEnumValEnd),
+                                "Use decimal form (e.g. (_ bv45 8) )")
+                     KLEE_LLVM_CL_VAL_END),
     llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL));
 
 llvm::cl::opt<bool> humanReadableSMTLIB(
@@ -44,8 +44,8 @@ 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"),
-                     clEnumValEnd),
+                                "Abbreviate with :named annotations")
+                     KLEE_LLVM_CL_VAL_END),
     llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET));
 }
 
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 45dc34bf..6438707a 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -92,8 +92,8 @@ namespace {
                         clEnumValN(eSwitchTypeLLVM, "llvm", 
                                    "lower using LLVM"),
                         clEnumValN(eSwitchTypeInternal, "internal", 
-                                   "execute switch internally"),
-                        clEnumValEnd),
+                                   "execute switch internally")
+                        KLEE_LLVM_CL_VAL_END),
              cl::init(eSwitchTypeInternal));
   
   cl::opt<bool>