up to 1.4.0+20171026

OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=32
2017-11-17 17:18:06 +00:00 · 2017-11-17 17:18:06 +00:00 · 3afdc30a7b
commit 3afdc30a7b
parent c36a5d68b2
29 changed files with 872 additions and 193 deletions
--- a/0001-Fix-generation-of-expressions-from-constant-sequenti.patch
+++ b/0001-Fix-generation-of-expressions-from-constant-sequenti.patch
@ -0,0 +1,31 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Sun, 29 Oct 2017 22:02:32 +0100
+Subject: Fix generation of expressions from constant sequential data
+Patch-mainline: no
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/ExecutorUtil.cpp | 6 ++++--
+ 1 file changed, 4 insertions(+), 2 deletions(-)
+
+diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
+index 53f4c5b85754..4f51ecb6301b 100644
+--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
+@@ -58,9 +58,11 @@ namespace klee {
+         return ConstantExpr::create(0, getWidthForLLVMType(c->getType()));
+       } else if (const ConstantDataSequential *cds =
+                  dyn_cast<ConstantDataSequential>(c)) {
+        // Handle a vector or array: first element has the smallest address,
+        // the last element the highest
+         std::vector<ref<Expr> > kids;
+-        for (unsigned i = 0, e = cds->getNumElements(); i != e; ++i) {
+-          ref<Expr> kid = evalConstant(cds->getElementAsConstant(i), ki);
+        for (unsigned i = cds->getNumElements(); i != 0; --i) {
+          ref<Expr> kid = evalConstant(cds->getElementAsConstant(i - 1), ki);
+           kids.push_back(kid);
+         }
+         ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data());
+-- 
+2.15.0
+
--- a/0001-errno-define-__errno_location.patch
+++ b/0001-errno-define-__errno_location.patch
@ -1,42 +0,0 @@
-From: Jiri Slaby <jirislaby@gmail.com>
-Date: Fri, 17 Mar 2017 13:15:18 +0100
-Subject: errno: define __errno_location
-Patch-mainline: no
-
-POSIX runtime library is built on my system with a reference to
-__errno_location(). And then it is undefined when klee is run
--with-posix:
-KLEE: NOTE: Using model: lib/libkleeRuntimePOSIX.bca
-KLEE: output directory is "test/Runtime/POSIX/Output/Read1.c.tmp.klee-out"
-KLEE: Using STP solver backend
-KLEE: WARNING: undefined reference to function: __errno_location
-KLEE: WARNING ONCE: calling external: __errno_location()
-KLEE: ERROR: (location information missing) ASSERTION FAIL: x == -1 && errno == EFAULT
-KLEE: NOTE: now ignoring this error at this location
-EXITING ON ERROR:
-Error: ASSERTION FAIL: x == -1 && errno == EFAULT
-Stack:
-       #000000170 in main (argc=4, argv=24928704)
-
-Therefore, the tests fail.
-
-Define __errno_location as a weak symbol to return the actual int errno.
-
-Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
- runtime/POSIX/errno_location.c |    9 +++++++++
- 1 file changed, 9 insertions(+)
- create mode 100644 runtime/POSIX/errno_location.c
-
--- /dev/null
-+++ b/runtime/POSIX/errno_location.c
-@@ -0,0 +1,9 @@
-+#include <errno.h>
-+
-+#undef errno
-+int errno __attribute__((weak));
-+
-+int __attribute__((weak)) *__errno_location(void)
-+{
-+	return &errno;
-+}
--- a/0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
+++ b/0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
@ -32,10 +32,10 @@ index ccf54ae13092..532051602fe3 100644
 #  define KLEE_LLVM_CL_VAL_END
 #else
 diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
-index 6c54d34b82bb..7d0707ddfab2 100644
+index 28546915b539..3558049d87cc 100644
 --- a/lib/Core/ExternalDispatcher.cpp
 +++ b/lib/Core/ExternalDispatcher.cpp
-@@ -319,6 +319,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
+@@ -324,6 +324,7 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
     Type *argTy =
         (i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType());
     Instruction *argI64p = GetElementPtrInst::Create(
@ -68,5 +68,5 @@ index b02605208bbb..54bda16013b6 100644
         }
         ii->removeFromParent();
 -- 
-2.14.2
+2.15.0

--- a/0001-test-DirSeek-make-it-XFAIL-temporarily.patch
+++ b/0001-test-DirSeek-make-it-XFAIL-temporarily.patch
@ -1,51 +0,0 @@
-From: Jiri Slaby <jirislaby@gmail.com>
-Date: Fri, 17 Mar 2017 13:40:30 +0100
-Subject: test: disable some tests temporarily
-Patch-mainline: no
-
-They fail for some reason I cannot debug ATM, I will fix it later.
-
-Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
- test/Feature/BitcastAlias.llvm37.ll     |    1 +
- test/Feature/BitcastAliasMD2U.llvm37.ll |    1 +
- test/Runtime/POSIX/DirSeek.c            |    1 +
- test/Runtime/POSIX/Ioctl.c              |    1 +
- 4 files changed, 4 insertions(+)
-
--- a/test/Feature/BitcastAlias.llvm37.ll
-+++ b/test/Feature/BitcastAlias.llvm37.ll
-@@ -1,4 +1,5 @@
- ; REQUIRES: geq-llvm-3.7
-+; REQUIRES: lt-llvm-4.0
- ; RUN: llvm-as %s -f -o %t1.bc
- ; RUN: rm -rf %t.klee-out
- ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
--- a/test/Feature/BitcastAliasMD2U.llvm37.ll
-+++ b/test/Feature/BitcastAliasMD2U.llvm37.ll
-@@ -1,4 +1,5 @@
- ; REQUIRES: geq-llvm-3.7
-+; REQUIRES: lt-llvm-4.0
- ; RUN: llvm-as %s -f -o %t1.bc
- ; RUN: rm -rf %t.klee-out
- ; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
--- a/test/Runtime/POSIX/DirSeek.c
-+++ b/test/Runtime/POSIX/DirSeek.c
-@@ -8,6 +8,7 @@
- // RUN: rm -rf %t.klee-out %t.klee-out-tmp
- // RUN: %gentmp %t.klee-out-tmp
- // RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2
-+// XFAIL: *
- 
- // For this test really to work as intended it needs to be run in a
- // directory large enough to cause uclibc to do multiple getdents
--- a/test/Runtime/POSIX/Ioctl.c
-+++ b/test/Runtime/POSIX/Ioctl.c
-@@ -1,6 +1,7 @@
- // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
- // RUN: rm -rf %t.klee-out
- // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t.bc --sym-files 0 4
-+// REQUIRES: undefined-symbol
- 
- #include <assert.h>
- #include <fcntl.h>
--- a/0002-Fix-getelementptr-for-array-or-vector-indices.patch
+++ b/0002-Fix-getelementptr-for-array-or-vector-indices.patch
@ -0,0 +1,100 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Sun, 29 Oct 2017 22:06:16 +0100
+Subject: Fix getelementptr for array or vector indices
+Patch-mainline: no
+
+Rewrote code based on: llvm::GEPOperator::accumulateConstantOffset():
+Handle signed offset correctly.
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/ExecutorUtil.cpp | 51 ++++++++++++++++++++++++-----------------------
+ 1 file changed, 26 insertions(+), 25 deletions(-)
+
+diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
+index 4f51ecb6301b..92dee5ac3906 100644
+--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
+@@ -19,18 +19,22 @@
+ #include "klee/Internal/Module/KModule.h"
+ 
+ #include "klee/Internal/Support/ErrorHandling.h"
+-#include "klee/util/GetElementPtrTypeIterator.h"
+ 
+-#include "llvm/IR/Function.h"
+ #include "llvm/IR/Constants.h"
+#include "llvm/IR/DataLayout.h"
+#include "llvm/IR/Function.h"
+ #include "llvm/IR/Instructions.h"
+ #include "llvm/IR/Module.h"
+-#include "llvm/IR/DataLayout.h"
+#include "llvm/IR/Operator.h"
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
+#include "llvm/Support/GetElementPtrTypeIterator.h"
+#else
+#include "llvm/IR/GetElementPtrTypeIterator.h"
+#endif
+ #include "llvm/Support/raw_ostream.h"
+ 
+ #include <cassert>
+ 
+-using namespace klee;
+ using namespace llvm;
+ 
+ namespace klee {
+@@ -188,34 +192,31 @@ namespace klee {
+ 
+     case Instruction::GetElementPtr: {
+       ref<ConstantExpr> base = op1->ZExt(Context::get().getPointerWidth());
+-
+       for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce);
+            ii != ie; ++ii) {
+-        ref<ConstantExpr> addend = 
+-          ConstantExpr::alloc(0, Context::get().getPointerWidth());
+-
+-        if (StructType *st = dyn_cast<StructType>(*ii)) {
+-          const StructLayout *sl = kmodule->targetData->getStructLayout(st);
+-          const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
+-
+-          addend = ConstantExpr::alloc(sl->getElementOffset((unsigned)
+-                                                            ci->getZExtValue()),
+-                                       Context::get().getPointerWidth());
+-        } else {
+-          const SequentialType *set = cast<SequentialType>(*ii);
+-          ref<ConstantExpr> index = 
+        ref<ConstantExpr> indexOp =
+             evalConstant(cast<Constant>(ii.getOperand()), ki);
+-          unsigned elementSize = 
+-            kmodule->targetData->getTypeStoreSize(set->getElementType());
+        if (indexOp->isZero())
+          continue;
+ 
+-          index = index->ZExt(Context::get().getPointerWidth());
+-          addend = index->Mul(ConstantExpr::alloc(elementSize, 
+-                                                  Context::get().getPointerWidth()));
+        // Handle a struct index, which adds its field offset to the pointer.
+        if (StructType *STy = dyn_cast<StructType>(*ii)) {
+          unsigned ElementIdx = indexOp->getZExtValue();
+          const StructLayout *SL = kmodule->targetData->getStructLayout(STy);
+          base = base->Add(
+              ConstantExpr::alloc(APInt(Context::get().getPointerWidth(),
+                                        SL->getElementOffset(ElementIdx))));
+          continue;
+         }
+ 
+-        base = base->Add(addend);
+        // For array or vector indices, scale the index by the size of the type.
+        // Indices can be negative
+        base = base->Add(indexOp->SExt(Context::get().getPointerWidth())
+                             ->Mul(ConstantExpr::alloc(
+                                 APInt(Context::get().getPointerWidth(),
+                                       kmodule->targetData->getTypeAllocSize(
+                                           ii.getIndexedType())))));
+       }
+-
+       return base;
+     }
+       
+-- 
+2.15.0
+
--- a/0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
+++ b/0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
@ -161,7 +161,7 @@ index 13e4f7d47e58..c597fa2a7b82 100644
     TLI = TM->getSubtargetImpl()->getTargetLowering();
 #else
 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
-index f1def38c90e5..5d1d0c22495c 100644
+index 4a820578bf16..f8706f9f74e5 100644
 --- a/tools/klee/main.cpp
 +++ b/tools/klee/main.cpp
@@ -35,6 +35,7 @@
@ -173,5 +173,5 @@ index f1def38c90e5..5d1d0c22495c 100644
 
 #include "llvm/Support/TargetSelect.h"
 -- 
-2.14.2
+2.15.0

--- a/0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
+++ b/0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
@ -0,0 +1,52 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Sun, 29 Oct 2017 22:12:30 +0100
+Subject: Fix correct element order of InsertElement/ExtractElement
+Patch-mainline: no
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/Executor.cpp | 21 ++++++---------------
+ 1 file changed, 6 insertions(+), 15 deletions(-)
+
+diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
+index 0b7aa1a97f68..dcb8d30e0ffa 100644
+--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
+@@ -2392,15 +2392,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
+     const unsigned elementCount = vt->getNumElements();
+     llvm::SmallVector<ref<Expr>, 8> elems;
+     elems.reserve(elementCount);
+-    for (unsigned i = 0; i < elementCount; ++i) {
+-      // evalConstant() will use ConcatExpr to build vectors with the
+-      // zero-th element leftmost (most significant bits), followed
+-      // by the next element (second leftmost) and so on. This means
+-      // that we have to adjust the index so we read left to right
+-      // rather than right to left.
+-      unsigned bitOffset = EltBits * (elementCount - i - 1);
+-      elems.push_back(i == iIdx ? newElt
+-                                : ExtractExpr::create(vec, bitOffset, EltBits));
+    for (unsigned i = elementCount; i != 0; --i) {
+      auto of = i - 1;
+      unsigned bitOffset = EltBits * of;
+      elems.push_back(
+          of == iIdx ? newElt : ExtractExpr::create(vec, bitOffset, EltBits));
+     }
+ 
+     ref<Expr> Result = ConcatExpr::createN(elementCount, elems.data());
+@@ -2430,12 +2426,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
+       return;
+     }
+ 
+-    // evalConstant() will use ConcatExpr to build vectors with the
+-    // zero-th element left most (most significant bits), followed
+-    // by the next element (second left most) and so on. This means
+-    // that we have to adjust the index so we read left to right
+-    // rather than right to left.
+-    unsigned bitOffset = EltBits*(vt->getNumElements() - iIdx -1);
+    unsigned bitOffset = EltBits * iIdx;
+     ref<Expr> Result = ExtractExpr::create(vec, bitOffset, EltBits);
+     bindLocal(ki, state, Result);
+     break;
+-- 
+2.15.0
+
--- a/0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
+++ b/0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
@ -1615,5 +1615,5 @@ index 000000000000..aa6b42ed6b9f
 +  return 0;
 +}
 -- 
-2.14.2
+2.15.0

--- a/0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
+++ b/0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
@ -0,0 +1,43 @@
+From: Martin Nowack <martin@se.inf.tu-dresden.de>
+Date: Tue, 25 Jul 2017 18:04:06 +0200
+Subject: Provide errno independent of CTYPE_EXTERNALS being defined
+Patch-mainline: no
+
+Add support for `errno()` for Darwin as well.
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/Executor.cpp | 12 +++++++++---
+ 1 file changed, 9 insertions(+), 3 deletions(-)
+
+diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
+index dcb8d30e0ffa..dd3af9836187 100644
+--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
+@@ -524,14 +524,20 @@ void Executor::initializeGlobals(ExecutionState &state) {
+     globalAddresses.insert(std::make_pair(f, addr));
+   }
+ 
+-  // Disabled, we don't want to promote use of live externals.
+-#ifdef HAVE_CTYPE_EXTERNALS
+ #ifndef WINDOWS
+-#ifndef DARWIN
+#ifndef __APPLE__
+   /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
+   int *errno_addr = __errno_location();
+#else
+  int *errno_addr = __error();
+#endif
+   addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
+#endif
+ 
+  // Disabled, we don't want to promote use of live externals.
+#ifdef HAVE_CTYPE_EXTERNALS
+#ifndef WINDOWS
+#ifndef DARWIN
+   /* from /usr/include/ctype.h:
+        These point into arrays of 384, so they can be indexed by any `unsigned
+        char' value [0,255]; by EOF (-1); or by any `signed char' value
+-- 
+2.15.0
+
--- a/0004-llvm37-handle-getRegisteredOptions.patch
+++ b/0004-llvm37-handle-getRegisteredOptions.patch
@ -12,7 +12,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 1 file changed, 4 insertions(+)

 diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
-index bffd3a4f7c00..ce09edde90ea 100644
+index aaba72f4b5b7..3c117db9fa7b 100644
 --- a/lib/Basic/CmdLineOptions.cpp
 +++ b/lib/Basic/CmdLineOptions.cpp
@@ -86,8 +86,12 @@ UseAssignmentValidatingSolver("debug-assignment-validating-solver",
@ -20,7 +20,7 @@ index bffd3a4f7c00..ce09edde90ea 100644
 
 void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
 +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
-+  StringMap<cl::Option*> &map = cl::getRegisteredOptions();
+  StringMap<cl::Option *> &map = cl::getRegisteredOptions();
 +#else
   StringMap<cl::Option *> map;
   cl::getRegisteredOptions(map);
@ -29,5 +29,5 @@ index bffd3a4f7c00..ce09edde90ea 100644
        i++) {
     if (i->second->Category != &Category) {
 -- 
-2.14.2
+2.15.0

--- a/0005-Track-errno-correctly.patch
+++ b/0005-Track-errno-correctly.patch
@ -0,0 +1,146 @@
+From: Martin Nowack <martin@se.inf.tu-dresden.de>
+Date: Tue, 25 Jul 2017 22:38:41 +0200
+Subject: Track errno correctly
+Patch-mainline: no
+
+Reduce the time of reading the value of errno
+and using it and writing it to the state space.
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/Executor.cpp           | 26 +++++++++++++++++++++++++-
+ lib/Core/ExternalDispatcher.cpp | 11 ++++++++++-
+ lib/Core/ExternalDispatcher.h   |  2 ++
+ lib/Core/Memory.h               |  3 +++
+ 4 files changed, 40 insertions(+), 2 deletions(-)
+
+diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
+index dd3af9836187..3492cd7e9b3c 100644
+--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
+@@ -531,7 +531,10 @@ void Executor::initializeGlobals(ExecutionState &state) {
+ #else
+   int *errno_addr = __error();
+ #endif
+-  addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
+  MemoryObject *errnoObj =
+      addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
+  // Copy values from and to program space explicitly
+  errnoObj->isUserSpecified = true;
+ #endif
+ 
+   // Disabled, we don't want to promote use of live externals.
+@@ -2973,6 +2976,27 @@ void Executor::callExternalFunction(ExecutionState &state,
+     return;
+   }
+ 
+#ifndef WINDOWS
+#ifndef __APPLE__
+  /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
+  int *errno_addr = __errno_location();
+#else
+  int *errno_addr = __error();
+#endif
+  // Update errno value explicitly
+  ObjectPair result;
+  bool resolved = state.addressSpace.resolveOne(
+      ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
+  if (!resolved)
+    klee_error("Could not resolve memory object for errno");
+  int error = externalDispatcher->getLastErrno();
+  if (memcmp(result.second->concreteStore, &error, result.first->size) != 0) {
+    ObjectState *wos =
+        state.addressSpace.getWriteable(result.first, result.second);
+    memcpy(wos->concreteStore, &error, result.first->size);
+  }
+#endif
+
+   Type *resultType = target->inst->getType();
+   if (resultType != Type::getVoidTy(function->getContext())) {
+     ref<Expr> e = ConstantExpr::fromMemory((void*) args, 
+diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
+index 6c54d34b82bb..28546915b539 100644
+--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
+@@ -65,6 +65,7 @@ private:
+   llvm::Module *singleDispatchModule;
+   std::vector<std::string> moduleIDs;
+   std::string &getFreshModuleID();
+  int lastErrno;
+ 
+ public:
+   ExternalDispatcherImpl(llvm::LLVMContext &ctx);
+@@ -72,6 +73,7 @@ public:
+   bool executeCall(llvm::Function *function, llvm::Instruction *i,
+                    uint64_t *args);
+   void *resolveSymbol(const std::string &name);
+  int getLastErrno();
+ };
+ 
+ std::string &ExternalDispatcherImpl::getFreshModuleID() {
+@@ -114,7 +116,8 @@ void *ExternalDispatcherImpl::resolveSymbol(const std::string &name) {
+   return addr;
+ }
+ 
+-ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) : ctx(ctx) {
+ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx)
+    : ctx(ctx), lastErrno(0) {
+   std::string error;
+   singleDispatchModule = new Module(getFreshModuleID(), ctx);
+ #if LLVM_VERSION_CODE < LLVM_VERSION(3, 6)
+@@ -253,6 +256,8 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) {
+     res = false;
+   } else {
+     executionEngine->runFunction(f, gvArgs);
+    // Explicitly acquire errno information
+    lastErrno = errno;
+     res = true;
+   }
+ 
+@@ -346,6 +351,8 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
+   return dispatcher;
+ }
+ 
+int ExternalDispatcherImpl::getLastErrno() { return lastErrno; }
+
+ ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx)
+     : impl(new ExternalDispatcherImpl(ctx)) {}
+ 
+@@ -359,4 +366,6 @@ bool ExternalDispatcher::executeCall(llvm::Function *function,
+ void *ExternalDispatcher::resolveSymbol(const std::string &name) {
+   return impl->resolveSymbol(name);
+ }
+
+int ExternalDispatcher::getLastErrno() { return impl->getLastErrno(); }
+ }
+diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h
+index c64dc7d81b93..e407355d6692 100644
+--- a/lib/Core/ExternalDispatcher.h
+++ b/lib/Core/ExternalDispatcher.h
+@@ -40,6 +40,8 @@ public:
+   bool executeCall(llvm::Function *function, llvm::Instruction *i,
+                    uint64_t *args);
+   void *resolveSymbol(const std::string &name);
+
+  int getLastErrno();
+ };
+ }
+ 
+diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
+index 4e5c87346917..afb41390d071 100644
+--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
+@@ -153,7 +153,10 @@ private:
+ 
+   const MemoryObject *object;
+ 
+public:
+   uint8_t *concreteStore;
+
+private:
+   // XXX cleanup name of flushMask (its backwards or something)
+   BitArray *concreteMask;
+ 
+-- 
+2.15.0
+
--- a/0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
+++ b/0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
@ -15,10 +15,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 7 files changed, 77 insertions(+), 9 deletions(-)

 diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
-index 673476f61042..cb8862813133 100644
+index 3492cd7e9b3c..51531f8f46c8 100644
 --- a/lib/Core/Executor.cpp
 +++ b/lib/Core/Executor.cpp
-@@ -2127,8 +2127,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
+@@ -2136,8 +2136,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FRem operation");
     llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
@ -248,7 +248,7 @@ index 64e4863f70b3..944f51ef336d 100644
     addPass(Passes, createLICMPass());               // Hoist loop invariants
     addPass(Passes, createGVNPass());                // Remove redundancies
 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
-index 5d1d0c22495c..c48570799a7f 100644
+index f8706f9f74e5..dbc166ed158a 100644
 --- a/tools/klee/main.cpp
 +++ b/tools/klee/main.cpp
@@ -291,7 +291,12 @@ KleeHandler::KleeHandler(int argc, char **argv)
@ -266,5 +266,5 @@ index 5d1d0c22495c..c48570799a7f 100644
       // create directory and try to link klee-last
       if (mkdir(d.c_str(), 0775) == 0) {
 -- 
-2.14.2
+2.15.0

--- a/0006-Declare-klee_get_errno-and-remove-local-declarations.patch
+++ b/0006-Declare-klee_get_errno-and-remove-local-declarations.patch
@ -0,0 +1,44 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Thu, 12 Oct 2017 17:58:00 +0200
+Subject: Declare klee_get_errno and remove local declarations
+Patch-mainline: no
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ include/klee/klee.h | 2 ++
+ runtime/POSIX/fd.c  | 6 ------
+ 2 files changed, 2 insertions(+), 6 deletions(-)
+
+diff --git a/include/klee/klee.h b/include/klee/klee.h
+index bd3100b5007e..282670eebc91 100644
+--- a/include/klee/klee.h
+++ b/include/klee/klee.h
+@@ -152,6 +152,8 @@ extern "C" {
+   /* Print range for given argument and tagged with name */
+   void klee_print_range(const char * name, int arg );
+ 
+  /* Get errno value of the current state */
+  int klee_get_errno(void);
+ #ifdef __cplusplus
+ }
+ #endif
+diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
+index 6f78c7475000..cf07d1380ef8 100644
+--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
+@@ -29,12 +29,6 @@
+ #include <sys/select.h>
+ #include <klee/klee.h>
+ 
+-/* #define DEBUG */
+-
+-void klee_warning(const char*);
+-void klee_warning_once(const char*);
+-int klee_get_errno(void);
+-
+ /* Returns pointer to the symbolic file structure fs the pathname is symbolic */
+ static exe_disk_file_t *__get_sym_file(const char *pathname) {
+   if (!pathname)
+-- 
+2.15.0
+
--- a/0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
+++ b/0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
@ -7,18 +7,18 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 ---
 lib/Core/Executor.cpp      | 16 ++++++++++++++++
 lib/Core/MemoryManager.cpp |  5 ++++-
- lib/Module/ModuleUtil.cpp  | 33 ++++++++++++++++++++++++++++++---
+ lib/Module/ModuleUtil.cpp  | 36 +++++++++++++++++++++++++++++++++---
 lib/Module/Optimize.cpp    | 28 ++++++++++++++++++++++++++++
 lib/Module/RaiseAsm.cpp    | 10 +++++++++-
 tools/kleaver/main.cpp     |  4 ++++
 tools/klee/main.cpp        |  4 ++++
- 7 files changed, 95 insertions(+), 5 deletions(-)
+ 7 files changed, 98 insertions(+), 5 deletions(-)

 diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
-index cb8862813133..aee0974c7792 100644
+index 51531f8f46c8..cd36eeec13e1 100644
 --- a/lib/Core/Executor.cpp
 +++ b/lib/Core/Executor.cpp
-@@ -1299,10 +1299,18 @@ void Executor::executeCall(ExecutionState &state,
+@@ -1308,10 +1308,18 @@ void Executor::executeCall(ExecutionState &state,
           //
           // Alignment requirements for scalar types is the same as their size
           if (argWidth > Expr::Int64) {
@ -37,7 +37,7 @@ index cb8862813133..aee0974c7792 100644
         }
       }
 
-@@ -1335,10 +1343,18 @@ void Executor::executeCall(ExecutionState &state,
+@@ -1344,10 +1352,18 @@ void Executor::executeCall(ExecutionState &state,
 
             Expr::Width argWidth = arguments[i]->getWidth();
             if (argWidth > Expr::Int64) {
@ -75,7 +75,7 @@ index 24e2ed97581f..f40e8bc9deb8 100644
     // Handle the case of 0-sized allocations as 1-byte allocations.
     // This way, we make sure we have this allocation between its own red zones
 diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
-index e6d592b135b6..8acada93c2cd 100644
+index e6d592b135b6..ee4af254dae2 100644
 --- a/lib/Module/ModuleUtil.cpp
 +++ b/lib/Module/ModuleUtil.cpp
@@ -196,7 +196,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
@ -91,7 +91,7 @@ index e6d592b135b6..8acada93c2cd 100644
   for (object::Archive::child_iterator AI = archive->child_begin(),
        AE = archive->child_end(); AI != AE; ++AI)
 #else
-@@ -236,7 +240,14 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
+@@ -236,7 +240,17 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
       return false;
     }
 
@ -100,14 +100,17 @@ index e6d592b135b6..8acada93c2cd 100644
 +    Expected<std::unique_ptr<llvm::object::Binary> > child =
 +      childErr->getAsBinary();
 +    if (!child) {
-+      ec = errorToErrorCode(child.takeError());
+      // I don't know why, but
+      // ec = errorToErrorCode(child.takeError())
+      // does not work here, so:
 +      consumeError(child.takeError());
+      ec = std::make_error_code(std::errc::io_error);
 +    }
 +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
     ErrorOr<std::unique_ptr<llvm::object::Binary> > child =
       childErr->getAsBinary();
     ec = child.getError();
-@@ -319,6 +330,13 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
+@@ -319,6 +333,13 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
     }
 
   }
@ -121,7 +124,7 @@ index e6d592b135b6..8acada93c2cd 100644
 
   KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n");
 
-@@ -490,7 +508,12 @@ Module *klee::linkWithLibrary(Module *module,
+@@ -490,7 +511,12 @@ Module *klee::linkWithLibrary(Module *module,
 #endif
 
   } else if (magic == sys::fs::file_magic::archive) {
@ -135,7 +138,7 @@ index e6d592b135b6..8acada93c2cd 100644
     ErrorOr<std::unique_ptr<object::Binary> > arch =
         object::createBinary(Buffer, &Context);
     ec = arch.getError();
-@@ -548,7 +571,11 @@ Function *klee::getDirectCallTarget(CallSite cs, bool moduleIsFullyLinked) {
+@@ -548,7 +574,11 @@ Function *klee::getDirectCallTarget(CallSite cs, bool moduleIsFullyLinked) {
     if (Function *f = dyn_cast<Function>(v)) {
       return f;
     } else if (llvm::GlobalAlias *ga = dyn_cast<GlobalAlias>(v)) {
@ -269,10 +272,10 @@ index b8b32e31264a..800cece95e9c 100644
   llvm::cl::ParseCommandLineOptions(argc, argv);
 
 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
-index c48570799a7f..d193d8341e93 100644
+index dbc166ed158a..3c78b480bb23 100644
 --- a/tools/klee/main.cpp
 +++ b/tools/klee/main.cpp
-@@ -1128,7 +1128,11 @@ int main(int argc, char **argv, char **envp) {
+@@ -1130,7 +1130,11 @@ int main(int argc, char **argv, char **envp) {
   llvm::InitializeNativeTarget();
 
   parseArguments(argc, argv);
@ -285,5 +288,5 @@ index c48570799a7f..d193d8341e93 100644
   if (Watchdog) {
     if (MaxTime==0) {
 -- 
-2.14.2
+2.15.0

--- a/0007-Add-support-for-modelling-errno_location.patch
+++ b/0007-Add-support-for-modelling-errno_location.patch
@ -0,0 +1,105 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Thu, 12 Oct 2017 21:57:03 +0200
+Subject: Add support for modelling errno_location
+Patch-mainline: no
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/SpecialFunctionHandler.cpp | 46 ++++++++++++++++++++++++++++++++++---
+ lib/Core/SpecialFunctionHandler.h   |  1 +
+ tools/klee/main.cpp                 |  2 ++
+ 3 files changed, 46 insertions(+), 3 deletions(-)
+
+diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
+index 88e0d1a034bd..a019a09486c1 100644
+--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
+@@ -89,6 +89,8 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
+   add("klee_define_fixed_object", handleDefineFixedObject, false),
+   add("klee_get_obj_size", handleGetObjSize, true),
+   add("klee_get_errno", handleGetErrno, true),
+  add("__errno_location", handleErrnoLocation, true),
+  add("__error", handleErrnoLocation, true),
+   add("klee_is_symbolic", handleIsSymbolic, true),
+   add("klee_make_symbolic", handleMakeSymbolic, false),
+   add("klee_mark_global", handleMarkGlobal, false),
+@@ -537,10 +539,48 @@ void SpecialFunctionHandler::handleGetErrno(ExecutionState &state,
+   // XXX should type check args
+   assert(arguments.size()==0 &&
+          "invalid number of arguments to klee_get_errno");
+-  executor.bindLocal(target, state,
+-                     ConstantExpr::create(errno, Expr::Int32));
+#ifndef WINDOWS
+#ifndef __APPLE__
+  int *errno_addr = __errno_location();
+#else
+  int *errno_addr = __error();
+#endif
+#else
+  int *errno_addr = nullptr;
+#endif
+
+  // Retrieve the memory object of the errno variable
+  ObjectPair result;
+  bool resolved = state.addressSpace.resolveOne(
+      ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
+  if (!resolved)
+    executor.terminateStateOnError(state, "Could not resolve address for errno",
+                                   Executor::User);
+  executor.bindLocal(target, state, result.second->read(0, Expr::Int32));
+}
+
+void SpecialFunctionHandler::handleErrnoLocation(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr> > &arguments) {
+  // Returns the address of the errno variable
+  assert(arguments.size() == 0 &&
+         "invalid number of arguments to __errno_location");
+
+#ifndef WINDOWS
+#ifndef __APPLE__
+  int *errno_addr = __errno_location();
+#else
+  int *errno_addr = __error();
+#endif
+#else
+  int *errno_addr = nullptr;
+#endif
+  executor.bindLocal(
+      target, state,
+      ConstantExpr::create((uint64_t)errno_addr,
+                           executor.kmodule->targetData->getTypeSizeInBits(
+                               target->inst->getType())));
+ }
+-
+ void SpecialFunctionHandler::handleCalloc(ExecutionState &state,
+                             KInstruction *target,
+                             std::vector<ref<Expr> > &arguments) {
+diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
+index 394b649aff72..5e58ede4f328 100644
+--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
+@@ -107,6 +107,7 @@ namespace klee {
+     HANDLER(handleDelete);    
+     HANDLER(handleDeleteArray);
+     HANDLER(handleExit);
+    HANDLER(handleErrnoLocation);
+     HANDLER(handleAliasFunction);
+     HANDLER(handleFree);
+     HANDLER(handleGetErrno);
+diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
+index f1def38c90e5..4a820578bf16 100644
+--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
+@@ -698,6 +698,8 @@ static const char *modelledExternals[] = {
+   "_assert",
+   "__assert_fail",
+   "__assert_rtn",
+  "__errno_location",
+  "__error",
+   "calloc",
+   "_exit",
+   "exit",
+-- 
+2.15.0
+
--- a/0007-llvm40-handle-different-header-names.patch
+++ b/0007-llvm40-handle-different-header-names.patch
@ -30,7 +30,7 @@ index 0439431b3bc8..ff76cd53c895 100644
 #include "llvm/IR/LLVMContext.h"
 #include "llvm/IR/Module.h"
 diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
-index 8acada93c2cd..63d3913a08f2 100644
+index ee4af254dae2..8aa070743048 100644
 --- a/lib/Module/ModuleUtil.cpp
 +++ b/lib/Module/ModuleUtil.cpp
@@ -26,7 +26,9 @@
@ -59,7 +59,7 @@ index 8acada93c2cd..63d3913a08f2 100644
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/Path.h"
 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
-index d193d8341e93..cd54d8aab5af 100644
+index 3c78b480bb23..d45fad22896f 100644
 --- a/tools/klee/main.cpp
 +++ b/tools/klee/main.cpp
@@ -31,7 +31,6 @@
@ -84,5 +84,5 @@ index d193d8341e93..cd54d8aab5af 100644
 #include <signal.h>
 #include <unistd.h>
 -- 
-2.14.2
+2.15.0

--- a/0008-Cleanup-test-cases.patch
+++ b/0008-Cleanup-test-cases.patch
@ -0,0 +1,42 @@
+From: Martin Nowack <martin_nowack@tu-dresden.de>
+Date: Thu, 12 Oct 2017 21:59:16 +0200
+Subject: Cleanup test cases
+Patch-mainline: no
+
+* remove assert(!errno): errno being 0 cannot be assumed if no error
+  occured
+* added missing header
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ test/Runtime/POSIX/DirSeek.c | 1 -
+ test/Runtime/POSIX/Ioctl.c   | 1 +
+ 2 files changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c
+index 3908b4e28879..155c80b92d1e 100644
+--- a/test/Runtime/POSIX/DirSeek.c
+++ b/test/Runtime/POSIX/DirSeek.c
+@@ -43,7 +43,6 @@ int main(int argc, char **argv) {
+   // Go to end, then back to 2nd
+   while (de)
+     de = readdir(d);
+-  assert(!errno);
+   seekdir(d, pos);
+   assert(telldir(d) == pos);
+   de = readdir(d);
+diff --git a/test/Runtime/POSIX/Ioctl.c b/test/Runtime/POSIX/Ioctl.c
+index e8220276f8be..f1caaf77dea2 100644
+--- a/test/Runtime/POSIX/Ioctl.c
+++ b/test/Runtime/POSIX/Ioctl.c
+@@ -5,6 +5,7 @@
+ #include <assert.h>
+ #include <fcntl.h>
+ #include <sys/stat.h>
+#include <sys/ioctl.h>
+ #include <termios.h>
+ #include <asm/ioctls.h>
+ #include <errno.h>
+-- 
+2.15.0
+
--- a/0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
+++ b/0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
@ -9,10 +9,10 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 1 file changed, 9 insertions(+)

 diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
-index aee0974c7792..08474ae700ac 100644
+index cd36eeec13e1..af7f680fec3d 100644
 --- a/lib/Core/Executor.cpp
 +++ b/lib/Core/Executor.cpp
-@@ -1442,12 +1442,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) {
+@@ -1451,12 +1451,21 @@ static bool isDebugIntrinsic(const Function *f, KModule *KM) {
 
 static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) {
   switch(width) {
@ -35,5 +35,5 @@ index aee0974c7792..08474ae700ac 100644
     return 0;
   }
 -- 
-2.14.2
+2.15.0

--- a/0009-llvm40-errorOr-and-similar.patch
+++ b/0009-llvm40-errorOr-and-similar.patch
@ -9,7 +9,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 1 file changed, 41 insertions(+), 9 deletions(-)

 diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
-index 63d3913a08f2..e49896a06718 100644
+index 8aa070743048..ad847de0b368 100644
 --- a/lib/Module/ModuleUtil.cpp
 +++ b/lib/Module/ModuleUtil.cpp
@@ -204,7 +204,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
@ -36,7 +36,7 @@ index 63d3913a08f2..e49896a06718 100644
     if (!ec) {
       memberName = memberNameErr.get();
 #else
-@@ -264,7 +270,10 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
+@@ -267,7 +273,10 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
 #endif
     if (ec) {
       // If we can't open as a binary object file its hopefully a bitcode file
@ -48,7 +48,7 @@ index 63d3913a08f2..e49896a06718 100644
       ErrorOr<MemoryBufferRef> buff = childErr->getMemoryBufferRef();
       ec = buff.getError();
 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-@@ -288,13 +297,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
+@@ -291,13 +300,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er
         Module *Result = 0;
         // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
@ -71,7 +71,7 @@ index 63d3913a08f2..e49896a06718 100644
         if (ec)
           errorMessage = ec.message();
         else
-@@ -471,7 +487,12 @@ Module *klee::linkWithLibrary(Module *module,
+@@ -474,7 +490,12 @@ Module *klee::linkWithLibrary(Module *module,
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 8)
     Module *Result = 0;
 #endif
@ -85,7 +85,7 @@ index 63d3913a08f2..e49896a06718 100644
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
     ErrorOr<std::unique_ptr<Module> > ResultErr =
 #else
-@@ -677,14 +698,22 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string
+@@ -680,14 +701,22 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string
     return nullptr;
   }
 
@ -111,7 +111,7 @@ index 63d3913a08f2..e49896a06718 100644
     return nullptr;
   }
   // The module has taken ownership of the MemoryBuffer so release it
-@@ -696,7 +725,10 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string
+@@ -699,7 +728,10 @@ Module *klee::loadModule(LLVMContext &ctx, const std::string &path, std::string
   auto module = *errorOrModule;
 #endif
 
@ -124,5 +124,5 @@ index 63d3913a08f2..e49896a06718 100644
 #else
   if (auto ec = module->materializeAllPermanently()) {
 -- 
-2.14.2
+2.15.0

--- a/0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
+++ b/0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
@ -0,0 +1,35 @@
+From: =?UTF-8?q?Julian=20B=C3=BCning?= <julian.buening@rwth-aachen.de>
+Date: Mon, 30 Oct 2017 18:53:40 +0100
+Subject: test: fix Feature/BFSSearcherAndDFSSearcherInterleaved.c
+Patch-mainline: no
+
+To use explicit enumeration of possible strings instead of CHECK-SAME
+(does not work as intended with LLVM >= 3.7).
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ test/Feature/BFSSearcherAndDFSSearcherInterleaved.c | 10 ++--------
+ 1 file changed, 2 insertions(+), 8 deletions(-)
+
+diff --git a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
+index 9cc11b709bbe..3dd5b4d59fe4 100644
+--- a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
+++ b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
+@@ -38,12 +38,6 @@ int main() {
+     }
+   }
+ 
+-  // exactly 4 characters
+-  // CHECK: {{^[A-D]{4}$}}
+-
+-  // for each of A, B, C and D: occurs exactly once
+-  // CHECK-SAME: {{^[B-D]*A[B-D]*$}}
+-  // CHECK-SAME: {{^[A,C-D]*B[A,C-D]*$}}
+-  // CHECK-SAME: {{^[A-B,D]*C[A-B,D]*$}}
+-  // CHECK-SAME: {{^[A-C]*D[A-C]*$}}
+  // exactly 4 characters, each of A, B, C and D occur exactly once
+  // CHECK: {{^(ABCD|ABDC|ACBD|ACDB|ADBC|ADCB|BACD|BADC|BCAD|BCDA|BDAC|BDCA|CABD|CADB|CBAD|CBDA|CDAB|CDBA|DABC|DACB|DBAC|DBCA|DCAB|DCBA)$}}
+ }
+-- 
+2.15.0
+
--- a/0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch
+++ b/0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch
@ -195,5 +195,5 @@ index da96981079ae..a223b39ada57 100644
 +
 +#endif
 -- 
-2.14.2
+2.15.0

--- a/0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
+++ b/0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
@ -9,8 +9,7 @@ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
 ---
 include/klee/util/GetElementPtrTypeIterator.h |  4 ++++
 lib/Core/Executor.cpp                         | 22 +++++++++++++++++++---
- lib/Core/ExecutorUtil.cpp                     | 17 ++++++++++++++---
- 3 files changed, 37 insertions(+), 6 deletions(-)
+ 2 files changed, 23 insertions(+), 3 deletions(-)

 diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
 index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
@ -28,7 +27,7 @@ index 5fb9f4ec5c2f..bf7cb6ff0bea 100644
         CurTy = 0;
       }
 diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
-index 08474ae700ac..5a88f1ae3180 100644
+index af7f680fec3d..f435f5389f64 100644
 --- a/lib/Core/Executor.cpp
 +++ b/lib/Core/Executor.cpp
@@ -2520,8 +2520,7 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
@ -67,41 +66,6 @@ index 08474ae700ac..5a88f1ae3180 100644
     index++;
   }
   kgepi->offset = constantOffset->getZExtValue();
-diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
-index 53f4c5b85754..6d18e07425c5 100644
--- a/lib/Core/ExecutorUtil.cpp
-+++ b/lib/Core/ExecutorUtil.cpp
-@@ -199,8 +199,7 @@ namespace klee {
-           addend = ConstantExpr::alloc(sl->getElementOffset((unsigned)
-                                                             ci->getZExtValue()),
-                                        Context::get().getPointerWidth());
-        } else {
-          const SequentialType *set = cast<SequentialType>(*ii);
-+        } else if (const SequentialType *set = dyn_cast<SequentialType>(*ii)) {
-           ref<ConstantExpr> index = 
-             evalConstant(cast<Constant>(ii.getOperand()), ki);
-           unsigned elementSize = 
-@@ -209,7 +208,19 @@ namespace klee {
-           index = index->ZExt(Context::get().getPointerWidth());
-           addend = index->Mul(ConstantExpr::alloc(elementSize, 
-                                                   Context::get().getPointerWidth()));
-        }
-+#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-+        } else if (const PointerType *ptr = dyn_cast<PointerType>(*ii)) {
-+          ref<ConstantExpr> index =
-+            evalConstant(cast<Constant>(ii.getOperand()));
-+          unsigned elementSize =
-+            kmodule->targetData->getTypeStoreSize(ptr->getElementType());
-+
-+          index = index->ZExt(Context::get().getPointerWidth());
-+          addend = index->Mul(ConstantExpr::alloc(elementSize,
-+                                                  Context::get().getPointerWidth()));
-+#endif
-+        } else
-+	  assert("invalid type" && 0);
- 
-         base = base->Add(addend);
-       }
 -- 
-2.14.2
+2.15.0

--- a/0012-llvm40-gep_type_iterator-has-no-operator.patch
+++ b/0012-llvm40-gep_type_iterator-has-no-operator.patch
@ -0,0 +1,32 @@
+From: Jiri Slaby <jirislaby@gmail.com>
+Date: Fri, 17 Nov 2017 17:56:18 +0100
+Subject: llvm40: gep_type_iterator has no operator*
+Patch-mainline: no
+
+Starting with LLVM 4.0, we have getStructTypeOrNull(), so use it.
+operator* in post-4 will have a different semantics.
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ lib/Core/ExecutorUtil.cpp | 4 ++++
+ 1 file changed, 4 insertions(+)
+
+diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
+index 92dee5ac3906..c9308795804e 100644
+--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
+@@ -200,7 +200,11 @@ namespace klee {
+           continue;
+ 
+         // Handle a struct index, which adds its field offset to the pointer.
+#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
+        if (StructType *STy = ii.getStructTypeOrNull()) {
+#else
+         if (StructType *STy = dyn_cast<StructType>(*ii)) {
+#endif
+           unsigned ElementIdx = indexOp->getZExtValue();
+           const StructLayout *SL = kmodule->targetData->getStructLayout(STy);
+           base = base->Add(
+-- 
+2.15.0
+
--- a/0013-llvm38-test-change-some-tests.patch
+++ b/0013-llvm38-test-change-some-tests.patch
@ -0,0 +1,123 @@
+From: Jiri Slaby <jirislaby@gmail.com>
+Date: Wed, 1 Nov 2017 09:25:47 +0100
+Subject: llvm38: test, change some tests
+Patch-mainline: no
+
+alias in LLVM 3.8 has a new format, it adds a AliaseeTy parameter. So
+handle this in the tests.
+
+Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
+---
+ test/Feature/BitcastAlias.llvm37.ll     |  1 +
+ test/Feature/BitcastAlias.llvm38.ll     | 35 +++++++++++++++++++++++++++++++++
+ test/Feature/BitcastAliasMD2U.llvm37.ll |  1 +
+ test/Feature/BitcastAliasMD2U.llvm38.ll | 35 +++++++++++++++++++++++++++++++++
+ 4 files changed, 72 insertions(+)
+ create mode 100644 test/Feature/BitcastAlias.llvm38.ll
+ create mode 100644 test/Feature/BitcastAliasMD2U.llvm38.ll
+
+diff --git a/test/Feature/BitcastAlias.llvm37.ll b/test/Feature/BitcastAlias.llvm37.ll
+index 0d6e72604d6b..3b702ba2a6b0 100644
+--- a/test/Feature/BitcastAlias.llvm37.ll
+++ b/test/Feature/BitcastAlias.llvm37.ll
+@@ -1,4 +1,5 @@
+ ; REQUIRES: geq-llvm-3.7
+; REQUIRES: lt-llvm-3.8
+ ; RUN: llvm-as %s -f -o %t1.bc
+ ; RUN: rm -rf %t.klee-out
+ ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+diff --git a/test/Feature/BitcastAlias.llvm38.ll b/test/Feature/BitcastAlias.llvm38.ll
+new file mode 100644
+index 000000000000..ff7009b7711b
+--- /dev/null
+++ b/test/Feature/BitcastAlias.llvm38.ll
+@@ -0,0 +1,35 @@
+; REQUIRES: geq-llvm-3.8
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+@foo = alias i32 (i32), i32 (i32)* @__foo
+
+define i32 @__foo(i32 %i) nounwind {
+entry:
+  ret i32 %i
+}
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+  %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+  %r = icmp eq i32 %call, 52
+  br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+  %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+  ret i32 0
+
+bbfalse:
+  %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+  ret i32 0
+}
+diff --git a/test/Feature/BitcastAliasMD2U.llvm37.ll b/test/Feature/BitcastAliasMD2U.llvm37.ll
+index 12abf09373f8..2332a1968dea 100644
+--- a/test/Feature/BitcastAliasMD2U.llvm37.ll
+++ b/test/Feature/BitcastAliasMD2U.llvm37.ll
+@@ -1,4 +1,5 @@
+ ; REQUIRES: geq-llvm-3.7
+; REQUIRES: lt-llvm-3.8
+ ; RUN: llvm-as %s -f -o %t1.bc
+ ; RUN: rm -rf %t.klee-out
+ ; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
+diff --git a/test/Feature/BitcastAliasMD2U.llvm38.ll b/test/Feature/BitcastAliasMD2U.llvm38.ll
+new file mode 100644
+index 000000000000..f4e41293c347
+--- /dev/null
+++ b/test/Feature/BitcastAliasMD2U.llvm38.ll
+@@ -0,0 +1,35 @@
+; REQUIRES: geq-llvm-3.8
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+@foo = alias i32 (i32), i32 (i32)* @__foo
+
+define i32 @__foo(i32 %i) nounwind {
+entry:
+  ret i32 %i
+}
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+  %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+  %r = icmp eq i32 %call, 52
+  br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+  %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+  ret i32 0
+
+bbfalse:
+  %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+  ret i32 0
+}
+-- 
+2.15.0
+
--- a/2
+++ b/2
@ -1,4 +1,4 @@
 <servicedata>
 <service name="tar_scm">
            <param name="url">git://github.com/klee/klee.git</param>
-          <param name="changesrevision">9f11eababd767b012b623806b40fa0647affa47e</param></service></servicedata>
+          <param name="changesrevision">9caaae0b1b6e52be3c7bb783f3a8be659a1a1869</param></service></servicedata>
--- a/klee-1.4.0+20171009.tar.xz
+++ b/klee-1.4.0+20171009.tar.xz
@ -1,3 +0,0 @@
-version https://git-lfs.github.com/spec/v1
-oid sha256:ad3ed763f431f001921a8b6bdab69e38de3f0f1e0746af6468b71a478a1dffee
-size 580524
--- a/klee-1.4.0+20171026.tar.xz
+++ b/klee-1.4.0+20171026.tar.xz
@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:a4a0830328c4cbac4f059a7fa016994df5101b5b9a30105fdf9cc42e5c14169e
+size 582380
--- a/klee.changes
+++ b/klee.changes
@ -1,3 +1,32 @@
+-------------------------------------------------------------------
+Fri Nov 17 17:01:38 UTC 2017 - jslaby@suse.com
+
+- Update to version 1.4.0+20171026:
+  * [cmake]Fix detection of non-standard path for tcmalloc
+  * fixing huge allocation size constant to be unsigned
+  * [travis] build metaSMT with C++11
+  * [travis] add a workaround to keep Travis alive when running tests for metaSMT-CVC4 (which needs around 10m for one specific test case)
+  * [travis] update scripts to additionally test CVC4 and Yices2
+  * [cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly
+  * add support for CVC4 and Yices2 via metaSMT
+  * Fixed assert in BFSSearcher that does not hold as part of interleaved searcher
+  * Removed unnecessary and redundant variable
+- removed
+  * 0001-errno-define-__errno_location.patch
+  * 0001-test-DirSeek-make-it-XFAIL-temporarily.patch
+- added
+  * 0001-Fix-generation-of-expressions-from-constant-sequenti.patch
+  * 0002-Fix-getelementptr-for-array-or-vector-indices.patch
+  * 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
+  * 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
+  * 0005-Track-errno-correctly.patch
+  * 0006-Declare-klee_get_errno-and-remove-local-declarations.patch
+  * 0007-Add-support-for-modelling-errno_location.patch
+  * 0008-Cleanup-test-cases.patch
+  * 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
+  * 0012-llvm40-gep_type_iterator-has-no-operator.patch
+  * 0013-llvm38-test-change-some-tests.patch
+
 -------------------------------------------------------------------
 Tue Oct 10 12:45:08 UTC 2017 - jslaby@suse.com

--- a/klee.spec
+++ b/klee.spec
@ -19,7 +19,7 @@
 %define llvm_version_minor 0
 %define llvm_version %{llvm_version_major}

-%define version_unconverted 1.4.0+20171009
+%define version_unconverted 1.4.0+20171026

 %ifarch %{ix86} x86_64
 %define with_uclibc 1
@ -31,26 +31,38 @@ Name:           klee
 Summary:        LLVM Execution Engine
 License:        NCSA
 Group:          Development/Languages/Other
-Version:        1.4.0+20171009
+Version:        1.4.0+20171026
 Release:        0
 Url:            http://klee.github.io/
 Source0:        %{name}-%{version}.tar.xz
 Source1:        %{name}-rpmlintrc
 Source2:        https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/not/not.cpp
 Source3:        https://raw.githubusercontent.com/llvm-mirror/llvm/release_%{llvm_version_major}%{llvm_version_minor}/utils/FileCheck/FileCheck.cpp
-Patch0:         0001-errno-define-__errno_location.patch
-Patch1:         0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
-Patch2:         0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
-Patch3:         0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
-Patch4:         0004-llvm37-handle-getRegisteredOptions.patch
-Patch5:         0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
-Patch6:         0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
-Patch7:         0007-llvm40-handle-different-header-names.patch
-Patch8:         0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
-Patch9:         0009-llvm40-errorOr-and-similar.patch
-Patch10:        0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch
-Patch11:        0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
-Patch14:        0001-test-DirSeek-make-it-XFAIL-temporarily.patch
+Patch1:         0001-Fix-generation-of-expressions-from-constant-sequenti.patch
+Patch2:         0002-Fix-getelementptr-for-array-or-vector-indices.patch
+Patch3:         0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch
+Patch4:         0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch
+Patch5:         0005-Track-errno-correctly.patch
+Patch6:         0006-Declare-klee_get_errno-and-remove-local-declarations.patch
+Patch7:         0007-Add-support-for-modelling-errno_location.patch
+Patch8:         0008-Cleanup-test-cases.patch
+Patch9:         0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch
+#---
+Patch10:        0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch
+Patch11:        0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch
+Patch12:        0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch
+Patch13:        0004-llvm37-handle-getRegisteredOptions.patch
+Patch14:        0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch
+Patch15:        0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch
+Patch16:        0007-llvm40-handle-different-header-names.patch
+Patch17:        0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch
+Patch18:        0009-llvm40-errorOr-and-similar.patch
+Patch19:        0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch
+Patch20:        0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch
+Patch21:        0012-llvm40-gep_type_iterator-has-no-operator.patch
+Patch22:        0013-llvm38-test-change-some-tests.patch
+#---
+Patch23:        0001-test-DirSeek-make-it-XFAIL-temporarily.patch

 BuildRequires:  clang%{llvm_version}
 BuildRequires:  cmake
@ -76,7 +88,7 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.

 %prep
 %setup -q
-%patch0 -p1
+#%%patch0 -p1
 %patch1 -p1
 %patch2 -p1
 %patch3 -p1
@ -88,7 +100,18 @@ information on what KLEE is and what it can do, see the OSDI 2008 paper.
 %patch9 -p1
 %patch10 -p1
 %patch11 -p1
+%patch12 -p1
+%patch13 -p1
 %patch14 -p1
+%patch15 -p1
+%patch16 -p1
+%patch17 -p1
+%patch18 -p1
+%patch19 -p1
+%patch20 -p1
+%patch21 -p1
+%patch22 -p1
+#%%patch23 -p1
 mkdir -p build/test/
 cp %{SOURCE2} build/test/
 cp %{SOURCE3} build/test/