about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--autoconf/configure.ac4
-rwxr-xr-xconfigure5
-rw-r--r--include/klee/Config/Version.h18
-rw-r--r--include/klee/Config/config.h.in5
-rw-r--r--include/klee/Internal/Module/KInstruction.h4
-rw-r--r--include/klee/Statistic.h4
-rw-r--r--include/klee/util/Bits.h4
-rw-r--r--include/klee/util/GetElementPtrTypeIterator.h3
-rw-r--r--lib/Core/Executor.cpp12
-rw-r--r--lib/Core/ExecutorUtil.cpp3
-rw-r--r--lib/Core/ExternalDispatcher.cpp12
-rw-r--r--lib/Core/StatsTracker.cpp7
-rw-r--r--lib/Core/TimingSolver.cpp3
-rw-r--r--lib/Expr/Expr.cpp3
-rw-r--r--lib/Expr/Parser.cpp5
-rw-r--r--lib/Module/Checks.cpp4
-rw-r--r--lib/Module/InstructionInfoTable.cpp12
-rw-r--r--lib/Module/IntrinsicCleaner.cpp8
-rw-r--r--lib/Module/KModule.cpp11
-rw-r--r--lib/Module/LowerSwitch.cpp3
-rw-r--r--lib/Module/ModuleUtil.cpp8
-rw-r--r--lib/Module/Optimize.cpp12
-rw-r--r--lib/Module/Passes.h14
-rw-r--r--lib/Module/RaiseAsm.cpp14
-rw-r--r--lib/Support/Time.cpp4
-rw-r--r--lib/Support/Timer.cpp4
-rw-r--r--tools/kleaver/main.cpp13
-rw-r--r--tools/klee/main.cpp16
28 files changed, 129 insertions, 86 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 57f16a2a..1ca3a61a 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -25,6 +25,10 @@ dnl Configure project makefiles
 dnl List every Makefile that exists within your source tree
 AC_CONFIG_HEADERS([include/klee/Config/config.h])
 
+AH_TOP([#ifndef KLEE_CONFIG_CONFIG_H
+#define KLEE_CONFIG_CONFIG_H])
+AH_BOTTOM([#endif])
+
 dnl FIXME: Make out of tree builds work.
 
 AC_LANG([C++])
diff --git a/configure b/configure
index 9d38f30b..fc3d35be 100755
--- a/configure
+++ b/configure
@@ -1795,6 +1795,11 @@ ac_config_headers="$ac_config_headers include/klee/Config/config.h"
 
 
 
+
+
+
+
+
 ac_ext=cpp
 ac_cpp='$CXXCPP $CPPFLAGS'
 ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
diff --git a/include/klee/Config/Version.h b/include/klee/Config/Version.h
new file mode 100644
index 00000000..f5adaa66
--- /dev/null
+++ b/include/klee/Config/Version.h
@@ -0,0 +1,18 @@
+//===-- Version.h -----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_CONFIG_VERSION_H
+#define KLEE_CONFIG_VERSION_H
+
+#include "klee/Config/config.h"
+
+#define LLVM_VERSION(major, minor) (((major) << 8) | (minor))
+#define LLVM_VERSION_CODE LLVM_VERSION(LLVM_VERSION_MAJOR, LLVM_VERSION_MINOR)
+
+#endif
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 653b27a4..023d04fe 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -1,5 +1,8 @@
 /* include/klee/Config/config.h.in.  Generated from autoconf/configure.tmp.ac by autoheader.  */
 
+#ifndef KLEE_CONFIG_CONFIG_H
+#define KLEE_CONFIG_CONFIG_H
+
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
@@ -74,3 +77,5 @@
 
 /* Define to 1 if you have the ANSI C header files. */
 #undef STDC_HEADERS
+
+#endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index f6becd4a..c96d103b 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_KINSTRUCTION_H
 #define KLEE_KINSTRUCTION_H
 
-#include "klee/Config/config.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/DataTypes.h"
 #else
 #include "llvm/Support/DataTypes.h"
diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h
index 6261fd95..f567f680 100644
--- a/include/klee/Statistic.h
+++ b/include/klee/Statistic.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_STATISTIC_H
 #define KLEE_STATISTIC_H
 
-#include "klee/Config/config.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/DataTypes.h"
 #else
 #include "llvm/Support/DataTypes.h"
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
index 06703604..f2bb7692 100644
--- a/include/klee/util/Bits.h
+++ b/include/klee/util/Bits.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_UTIL_BITS_H
 #define KLEE_UTIL_BITS_H
 
-#include "klee/Config/config.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/DataTypes.h"
 #else
 #include "llvm/Support/DataTypes.h"
diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
index c552595c..302c19ef 100644
--- a/include/klee/util/GetElementPtrTypeIterator.h
+++ b/include/klee/util/GetElementPtrTypeIterator.h
@@ -21,7 +21,8 @@
 #include "llvm/User.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Instructions.h"
-#if (LLVM_VERSION_MAJOR > 2)
+#include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
 #include "llvm/Constants.h"
 #endif
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1826a4d6..e46ff9b0 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -34,7 +34,7 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/util/GetElementPtrTypeIterator.h"
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Module/Cell.h"
@@ -50,7 +50,7 @@
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
@@ -58,7 +58,7 @@
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
 #include "llvm/Support/Process.h"
@@ -1309,7 +1309,7 @@ Function* Executor::getCalledFunction(CallSite &cs, ExecutionState &state) {
 }
 
 static bool isDebugIntrinsic(const Function *f, KModule *KM) {
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   // Fast path, getIntrinsicID is slow.
   if (f == KM->dbgStopPointFn)
     return true;
@@ -1846,7 +1846,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
  
     // Memory instructions...
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   case Instruction::Malloc:
   case Instruction::Alloca: {
     AllocationInst *ai = cast<AllocationInst>(i);
@@ -1866,7 +1866,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     executeAlloc(state, size, isLocal, ki);
     break;
   }
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   case Instruction::Free: {
     executeFree(state, eval(ki, 0, state).value);
     break;
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 5f974725..02f18bb4 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -15,6 +15,7 @@
 #include "klee/Interpreter.h"
 #include "klee/Solver.h"
 
+#include "klee/Config/Version.h"
 #include "klee/Internal/Module/KModule.h"
 
 #include "klee/util/GetElementPtrTypeIterator.h"
@@ -23,7 +24,7 @@
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
 #include "llvm/ModuleProvider.h"
 #endif
 #include "llvm/Support/CallSite.h"
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index bc68ce0d..5c03e42d 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -8,7 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "ExternalDispatcher.h"
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 
 // Ugh.
 #undef PACKAGE_BUGREPORT
@@ -21,16 +21,16 @@
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Instructions.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
 #include "llvm/ModuleProvider.h"
 #endif
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/ExecutionEngine/JIT.h"
 #include "llvm/ExecutionEngine/GenericValue.h"
 #include "llvm/Support/CallSite.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/DynamicLibrary.h"
 #else
 #include "llvm/Support/DynamicLibrary.h"
@@ -85,12 +85,12 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) {
 
 ExternalDispatcher::ExternalDispatcher() {
   dispatchModule = new Module("ExternalDispatcher", getGlobalContext());
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   ExistingModuleProvider* MP = new ExistingModuleProvider(dispatchModule);
 #endif
 
   std::string error;
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   executionEngine = ExecutionEngine::createJIT(MP, &error);
 #else
   executionEngine = ExecutionEngine::createJIT(dispatchModule, &error);
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 03d5e926..7dcca6b2 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -13,6 +13,7 @@
 
 #include "klee/ExecutionState.h"
 #include "klee/Statistics.h"
+#include "klee/Config/Version.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Module/KInstruction.h"
@@ -35,12 +36,12 @@
 #include "llvm/Type.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/CFG.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
 #include "llvm/Support/Process.h"
 #endif
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Path.h"
 #else
 #include "llvm/Support/Path.h"
@@ -282,7 +283,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
         //
         // FIXME: This trick no longer works, we should fix this in the line
         // number propogation.
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
         if (isa<DbgStopPointInst>(inst))
 #endif
           es.coveredLines[&ii.file].insert(ii.line);
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index d0aa3f6a..d2c07f46 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -9,13 +9,14 @@
 
 #include "TimingSolver.h"
 
+#include "klee/Config/Version.h"
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
 
 #include "CoreStats.h"
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
 #include "llvm/Support/Process.h"
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 08d5cd27..420eaa90 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -8,6 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Expr.h"
+#include "klee/Config/Version.h"
 
 #include "llvm/Support/CommandLine.h"
 // FIXME: We shouldn't need this once fast constant support moves into
@@ -346,7 +347,7 @@ void ConstantExpr::toString(std::string &Res) const {
 ref<ConstantExpr> ConstantExpr::Concat(const ref<ConstantExpr> &RHS) {
   Expr::Width W = getWidth() + RHS->getWidth();
   APInt Tmp(value);
-#if (LLVM_VERSION_MAJOR <= 2 && LLVM_VERSION_MINOR <= 8)
+#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8)
   Tmp.zext(W);
 #else
   Tmp=Tmp.zext(W);
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index a41c5624..a94d5614 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -11,6 +11,7 @@
 
 #include "expr/Lexer.h"
 
+#include "klee/Config/Version.h"
 #include "klee/Constraints.h"
 #include "klee/ExprBuilder.h"
 #include "klee/Solver.h"
@@ -1496,13 +1497,13 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
     Val = -Val;
 
   if (Type < Val.getBitWidth())
-#if (LLVM_VERSION_MAJOR < 3)
+#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8)
     Val.trunc(Type);
 #else
     Val=Val.trunc(Type);
 #endif
   else if (Type > Val.getBitWidth())
-#if (LLVM_VERSION_MAJOR < 3)
+#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8)
     Val.zext(Type);
 #else
     Val=Val.zext(Type);
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 2edcf940..c2f98c0f 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -9,6 +9,8 @@
 
 #include "Passes.h"
 
+#include "klee/Config/Version.h"
+
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Function.h"
@@ -16,7 +18,7 @@
 #include "llvm/Instruction.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index e08dc2b3..0e193452 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -7,15 +7,15 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Config/config.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
+#include "klee/Config/Version.h"
 
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
 #include "llvm/Linker.h"
 #include "llvm/Module.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
 #include "llvm/Assembly/AsmAnnotationWriter.h"
 #else
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
@@ -24,7 +24,7 @@
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/InstIterator.h"
 #include "llvm/Support/raw_ostream.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/Analysis/DebugInfo.h"
 #endif
 #include "llvm/Analysis/ValueTracking.h"
@@ -37,7 +37,7 @@ using namespace klee;
 
 class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter {
 public:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   void emitInstructionAnnot(const Instruction *i, llvm::raw_ostream &os) {
 #else
   void emitInstructionAnnot(const Instruction *i,
@@ -74,7 +74,7 @@ static void buildInstructionToLineMap(Module *m,
   }
 }
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
 static std::string getDSPIPath(const DbgStopPointInst *dspi) {
   std::string dir, file;
   bool res = GetConstantStringInfo(dspi->getDirectory(), dir);
@@ -98,7 +98,7 @@ static std::string getDSPIPath(DILocation Loc) {
 bool InstructionInfoTable::getInstructionDebugInfo(const llvm::Instruction *I, 
                                                    const std::string *&File,
                                                    unsigned &Line) {
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   if (const DbgStopPointInst *dspi = dyn_cast<DbgStopPointInst>(I)) {
     File = internString(getDSPIPath(dspi));
     Line = dspi->getLine();
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index da0c65f8..8e326af9 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -9,7 +9,7 @@
 
 #include "Passes.h"
 
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Function.h"
@@ -17,7 +17,7 @@
 #include "llvm/Instruction.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
@@ -61,7 +61,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         // FIXME: This is much more target dependent than just the word size,
         // however this works for x86-32 and x86-64.
       case Intrinsic::vacopy: { // (dst, src) -> *((i8**) dst) = *((i8**) src)
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
         Value *dst = ii->getOperand(1);
         Value *src = ii->getOperand(2);
 #else
@@ -94,7 +94,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         break;
       }
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
       case Intrinsic::dbg_stoppoint: {
         // We can remove this stoppoint if the next instruction is
         // sure to be another stoppoint. This is nice for cleanliness
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 0364127d..94c3d05b 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -14,6 +14,7 @@
 
 #include "Passes.h"
 
+#include "klee/Config/Version.h"
 #include "klee/Interpreter.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
@@ -22,7 +23,7 @@
 
 #include "llvm/Bitcode/ReaderWriter.h"
 #include "llvm/Instructions.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
@@ -31,10 +32,10 @@
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/Support/raw_os_ostream.h"
 #endif
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Path.h"
 #else
 #include "llvm/Support/Path.h"
@@ -230,7 +231,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
       BasicBlock *exit = BasicBlock::Create(getGlobalContext(), "exit", f);
       PHINode *result = 0;
       if (f->getReturnType() != Type::getVoidTy(getGlobalContext()))
-#if (LLVM_VERSION_MAJOR > 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
         result = PHINode::Create(f->getReturnType(), 0, "retval", exit);
 #else
 		result = PHINode::Create(f->getReturnType(), "retval", exit);
@@ -341,7 +342,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     std::ostream *os = ih->openOutputFile("assembly.ll");
     assert(os && os->good() && "unable to open source output");
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 6)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 6)
     // We have an option for this in case the user wants a .ll they
     // can compile.
     if (NoTruncateSourceLines) {
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 7d6920be..6667a006 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -15,7 +15,8 @@
 //===----------------------------------------------------------------------===//
 
 #include "Passes.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include <algorithm>
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 11f2b2c5..029540ae 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -8,14 +8,14 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Internal/Support/ModuleUtil.h"
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
 #include "llvm/Linker.h"
 #include "llvm/Module.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
 #include "llvm/Assembly/AsmAnnotationWriter.h"
 #else
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
@@ -25,7 +25,7 @@
 #include "llvm/Support/InstIterator.h"
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Analysis/ValueTracking.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Path.h"
 #else
 #include "llvm/Support/Path.h"
@@ -72,7 +72,7 @@ Function *klee::getDirectCallTarget(CallSite cs) {
 }
 
 static bool valueIsOnlyCalled(const Value *v) {
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   for (Value::use_const_iterator it = v->use_begin(), ie = v->use_end();
        it != ie; ++it) {
 #else
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index 633c21a1..e0ae4d99 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -15,14 +15,14 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "llvm/Module.h"
 #include "llvm/PassManager.h"
 #include "llvm/Analysis/Passes.h"
 #include "llvm/Analysis/LoopPass.h"
 #include "llvm/Analysis/Verifier.h"
 #include "llvm/Support/CommandLine.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/DynamicLibrary.h"
 #else
 #include "llvm/Support/DynamicLibrary.h"
@@ -99,7 +99,7 @@ static void AddStandardCompilePasses(PassManager &PM) {
 
   if (DisableOptimizations) return;
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   addPass(PM, createRaiseAllocationsPass());     // call %malloc -> malloc inst
 #endif
   addPass(PM, createCFGSimplificationPass());    // Clean up disgusting code
@@ -124,7 +124,7 @@ static void AddStandardCompilePasses(PassManager &PM) {
   addPass(PM, createCFGSimplificationPass());    // Merge & remove BBs
   addPass(PM, createScalarReplAggregatesPass()); // Break up aggregate allocas
   addPass(PM, createInstructionCombiningPass()); // Combine silly seq's
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   addPass(PM, createCondPropagationPass());      // Propagate conditionals
 #endif
 
@@ -134,7 +134,7 @@ static void AddStandardCompilePasses(PassManager &PM) {
   addPass(PM, createLoopRotatePass());
   addPass(PM, createLICMPass());                 // Hoist loop invariants
   addPass(PM, createLoopUnswitchPass());         // Unswitch loops.
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
   addPass(PM, createLoopIndexSplitPass());       // Index split loops.
 #endif
   // FIXME : Removing instcombine causes nestedloop regression.
@@ -150,7 +150,7 @@ static void AddStandardCompilePasses(PassManager &PM) {
   // Run instcombine after redundancy elimination to exploit opportunities
   // opened up by them.
   addPass(PM, createInstructionCombiningPass());
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   addPass(PM, createCondPropagationPass());      // Propagate conditionals
 #endif
 
diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h
index 2b1ea9bc..480fbde6 100644
--- a/lib/Module/Passes.h
+++ b/lib/Module/Passes.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_PASSES_H
 #define KLEE_PASSES_H
 
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 
 #include "llvm/Constants.h"
 #include "llvm/Instructions.h"
@@ -34,7 +34,7 @@ namespace klee {
 class RaiseAsmPass : public llvm::ModulePass {
   static char ID;
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR >= 9)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
   const llvm::TargetLowering *TLI;
 #endif
 
@@ -51,7 +51,7 @@ class RaiseAsmPass : public llvm::ModulePass {
   bool runOnInstruction(llvm::Module &M, llvm::Instruction *I);
 
 public:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   RaiseAsmPass() : llvm::ModulePass((intptr_t) &ID) {}
 #else
   RaiseAsmPass() : llvm::ModulePass(ID) {}
@@ -72,7 +72,7 @@ class IntrinsicCleanerPass : public llvm::ModulePass {
 public:
   IntrinsicCleanerPass(const llvm::TargetData &TD,
                        bool LI=true)
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
     : llvm::ModulePass((intptr_t) &ID),
 #else
     : llvm::ModulePass(ID),
@@ -101,7 +101,7 @@ class PhiCleanerPass : public llvm::FunctionPass {
   static char ID;
 
 public:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   PhiCleanerPass() : llvm::FunctionPass((intptr_t) &ID) {}
 #else
   PhiCleanerPass() : llvm::FunctionPass(ID) {}
@@ -113,7 +113,7 @@ public:
 class DivCheckPass : public llvm::ModulePass {
   static char ID;
 public:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   DivCheckPass(): ModulePass((intptr_t) &ID) {}
 #else
   DivCheckPass(): ModulePass(ID) {}
@@ -127,7 +127,7 @@ public:
 class LowerSwitchPass : public llvm::FunctionPass {
 public:
   static char ID; // Pass identification, replacement for typeid
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
   LowerSwitchPass() : FunctionPass((intptr_t) &ID) {} 
 #else
   LowerSwitchPass() : FunctionPass(ID) {} 
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index 76a4f242..8f862ffa 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -8,13 +8,13 @@
 //===----------------------------------------------------------------------===//
 
 #include "Passes.h"
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 
 #include "llvm/InlineAsm.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR >= 9)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/Host.h"
 #include "llvm/Target/TargetLowering.h"
@@ -38,7 +38,7 @@ Function *RaiseAsmPass::getIntrinsic(llvm::Module &M,
 bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) {
   if (CallInst *ci = dyn_cast<CallInst>(I)) {
     if (InlineAsm *ia = dyn_cast<InlineAsm>(ci->getCalledValue())) {
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR >= 9)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
       (void) ia;
       return TLI && TLI->ExpandInlineAsm(ci);
 #else
@@ -47,7 +47,7 @@ bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) {
       const llvm::Type *T = ci->getType();
 
       // bswaps
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
       unsigned NumOperands = ci->getNumOperands();
       llvm::Value *Arg0 = NumOperands > 1 ? ci->getOperand(1) : 0;
 #else
@@ -62,7 +62,7 @@ bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) {
             as == "rorw $$8, ${0:w};rorl $$16, $0;rorw $$8, ${0:w}" &&
             cs == "=r,0,~{dirflag},~{fpsr},~{flags},~{cc}"))) {
         Function *F = getIntrinsic(M, Intrinsic::bswap, Arg0->getType());
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 8)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
         ci->setOperand(0, F);
 #else
         ci->setCalledFunction(F);
@@ -79,7 +79,7 @@ bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) {
 bool RaiseAsmPass::runOnModule(Module &M) {
   bool changed = false;
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR >= 9)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
   std::string Err;
   std::string HostTriple = llvm::sys::getHostTriple();
   const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err);
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index ebcc390a..fb0e349c 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -7,10 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "klee/Internal/System/Time.h"
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
 #include "llvm/Support/Process.h"
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index c51815aa..35922d4d 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -7,10 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "klee/Internal/Support/Timer.h"
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
 #include "llvm/Support/Process.h"
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 0581ea27..0c4a78f7 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -3,6 +3,7 @@
 #include "expr/Lexer.h"
 #include "expr/Parser.h"
 
+#include "klee/Config/Version.h"
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/ExprBuilder.h"
@@ -25,7 +26,7 @@
 #undef PACKAGE_TARNAME
 #undef PACKAGE_VERSION
 
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Signals.h"
 #else
 #include "llvm/Support/Signals.h"
@@ -283,7 +284,7 @@ int main(int argc, char **argv) {
 
   std::string ErrorStr;
   
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
   MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr);
   if (!MB) {
     std::cerr << argv[0] << ": error: " << ErrorStr << "\n";
@@ -316,14 +317,14 @@ int main(int argc, char **argv) {
 
   switch (ToolAction) {
   case PrintTokens:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
     PrintInputTokens(MB);
 #else
     PrintInputTokens(MB.get());
 #endif
     break;
   case PrintAST:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
     success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB,
                             Builder);
 #else
@@ -332,7 +333,7 @@ int main(int argc, char **argv) {
 #endif
     break;
   case Evaluate:
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
     success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
                                MB, Builder);
 #else
@@ -345,7 +346,7 @@ int main(int argc, char **argv) {
   }
 
   delete Builder;
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
   delete MB;
 #endif
   llvm::llvm_shutdown();
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index e37eb00a..12f90f2a 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -7,7 +7,7 @@
 #include "klee/Expr.h"
 #include "klee/Interpreter.h"
 #include "klee/Statistics.h"
-#include "klee/Config/config.h"
+#include "klee/Config/Version.h"
 #include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/TreeStream.h"
 #include "klee/Internal/Support/ModuleUtil.h"
@@ -15,14 +15,14 @@
 
 #include "llvm/Constants.h"
 #include "llvm/Module.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
 #include "llvm/ModuleProvider.h"
 #endif
 #include "llvm/Type.h"
 #include "llvm/InstrTypes.h"
 #include "llvm/Instruction.h"
 #include "llvm/Instructions.h"
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Bitcode/ReaderWriter.h"
@@ -37,7 +37,7 @@
 #undef PACKAGE_TARNAME
 #undef PACKAGE_VERSION
 #include "llvm/Target/TargetSelect.h"
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Signals.h"
 #else
 #include "llvm/Support/Signals.h"
@@ -526,7 +526,7 @@ void KleeHandler::getOutFiles(std::string path,
   }
   for (std::set<llvm::sys::Path>::iterator it = contents.begin(),
          ie = contents.end(); it != ie; ++it) {
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR == 6)
+#if LLVM_VERSION_CODE != LLVM_VERSION(2, 6)
     std::string f = it->str();
 #else
     std::string f = it->toString();
@@ -1148,7 +1148,7 @@ int main(int argc, char **argv, char **envp) {
   sys::SetInterruptFunction(interrupt_handle);
 
   // Load the bytecode...
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 7)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
   std::string ErrorMsg;
   ModuleProvider *MP = 0;
   if (MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg)) {
@@ -1165,7 +1165,7 @@ int main(int argc, char **argv, char **envp) {
 #endif
   std::string ErrorMsg;
   Module *mainModule = 0;
-#if (LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
   MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg);
   if (Buffer) {
     mainModule = getLazyBitcodeModule(Buffer, getGlobalContext(), &ErrorMsg);
@@ -1464,7 +1464,7 @@ int main(int argc, char **argv, char **envp) {
   std::cerr << stats.str();
   handler->getInfoStream() << stats.str();
 
-#if !(LLVM_VERSION_MAJOR == 2 && LLVM_VERSION_MINOR < 9)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
   BufferPtr.take();
 #endif
   delete handler;