about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--.travis.yml5
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/StatsTracker.cpp21
-rw-r--r--lib/Core/TimingSolver.cpp32
-rw-r--r--lib/Module/Checks.cpp4
-rw-r--r--lib/Module/InstructionInfoTable.cpp4
-rw-r--r--lib/Module/KModule.cpp12
-rw-r--r--lib/Module/LowerSwitch.cpp2
-rw-r--r--lib/Module/RaiseAsm.cpp2
-rw-r--r--lib/Solver/Z3Solver.h2
-rw-r--r--lib/Support/TreeStream.cpp8
-rw-r--r--tools/klee/main.cpp12
-rw-r--r--unittests/CMakeLists.txt1
-rw-r--r--unittests/Makefile2
-rw-r--r--unittests/TreeStream/CMakeLists.txt3
-rw-r--r--unittests/TreeStream/Makefile11
-rw-r--r--unittests/TreeStream/TreeStreamTest.cpp48
17 files changed, 113 insertions, 69 deletions
diff --git a/.travis.yml b/.travis.yml
index 9a337952..09147e38 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -107,7 +107,10 @@ addons:
     - libselinux1-dev
     - cmake
 
-cache: apt
+cache: 
+  apt: true
+  directories:
+    - $HOME/Library/Caches/Homebrew
 before_install:
     ###########################################################################
     # Set up the locations to get various packages from
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 884f388d..ff842fd1 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -548,7 +548,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
   // ensures that we won't conflict. we don't need to allocate a memory object
   // since reading/writing via a function pointer is unsupported anyway.
   for (Module::iterator i = m->begin(), ie = m->end(); i != ie; ++i) {
-    Function *f = static_cast<Function *>(i);
+    Function *f = &*i;
     ref<ConstantExpr> addr(0);
 
     // If the symbol has external weak linkage then it is implicitly
@@ -602,7 +602,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
   for (Module::const_global_iterator i = m->global_begin(),
          e = m->global_end();
        i != e; ++i) {
-    const GlobalVariable *v = static_cast<const GlobalVariable *>(i);
+    const GlobalVariable *v = &*i;
     size_t globalObjectAlignment = getAllocationAlignment(v);
     if (i->isDeclaration()) {
       // FIXME: We have no general way of handling unknown external
@@ -680,8 +680,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
        i != ie; ++i) {
     // Map the alias to its aliasee's address. This works because we have
     // addresses for everything, even undefined functions. 
-    globalAddresses.insert(std::make_pair(static_cast<GlobalAlias *>(i),
-	  evalConstant(i->getAliasee())));
+    globalAddresses.insert(std::make_pair(&*i, evalConstant(i->getAliasee())));
   }
 
   // once all objects are allocated, do the actual initialization
@@ -689,7 +688,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
          e = m->global_end();
        i != e; ++i) {
     if (i->hasInitializer()) {
-      const GlobalVariable *v = static_cast<const GlobalVariable *>(i);
+      const GlobalVariable *v = &*i;
       MemoryObject *mo = globalObjects.find(v)->second;
       const ObjectState *os = state.addressSpace.findObject(mo);
       assert(os);
@@ -1264,7 +1263,7 @@ void Executor::printDebugInstructions(ExecutionState &state) {
     (*stream) << ":";
   }
 
-  (*stream) << state.pc->info->id;
+  (*stream) << state.pc->info->assemblyLine;
 
   if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
       optionIsSet(DebugPrintInstructions, FILE_ALL))
@@ -3640,7 +3639,7 @@ void Executor::runFunctionAsMain(Function *f,
   if (ai!=ae) {
     arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
     if (++ai!=ae) {
-      Instruction *first = static_cast<Instruction *>(f->begin()->begin());
+      Instruction *first = &*(f->begin()->begin());
       argvMO =
           memory->allocate((argc + 1 + envc + 1 + 1) * NumPtrBytes,
                            /*isLocal=*/false, /*isGlobal=*/true,
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index b93796ec..addb3de6 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -165,7 +165,7 @@ static bool instructionIsCoverable(Instruction *i) {
     if (it==bb->begin()) {
       return true;
     } else {
-      Instruction *prev = static_cast<Instruction *>(--it);
+      Instruction *prev = &*(--it);
       if (isa<CallInst>(prev) || isa<InvokeInst>(prev)) {
         Function *target =
             getDirectCallTarget(CallSite(prev), /*moduleIsFullyLinked=*/true);
@@ -542,7 +542,7 @@ void StatsTracker::writeIStats() {
       // Always try to write the filename before the function name, as otherwise
       // KCachegrind can create two entries for the function, one with an
       // unnamed file and one without.
-      Function *fn = static_cast<Function *>(fnIt);
+      Function *fn = &*fnIt;
       const InstructionInfo &ii = executor.kmodule->infos->getFunctionInfo(fn);
       if (ii.file != sourceFile) {
         of << "fl=" << ii.file << "\n";
@@ -639,9 +639,9 @@ static std::vector<Instruction*> getSuccs(Instruction *i) {
 
   if (i==bb->getTerminator()) {
     for (succ_iterator it = succ_begin(bb), ie = succ_end(bb); it != ie; ++it)
-      res.push_back(static_cast<Instruction *>(it->begin()));
+      res.push_back(&*(it->begin()));
   } else {
-    res.push_back(static_cast<Instruction *>(++BasicBlock::iterator(i)));
+    res.push_back(&*(++BasicBlock::iterator(i)));
   }
 
   return res;
@@ -688,7 +688,7 @@ void StatsTracker::computeReachableUncovered() {
            bbIt != bb_ie; ++bbIt) {
         for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
              it != ie; ++it) {
-          Instruction *inst = static_cast<Instruction *>(it);
+          Instruction *inst = &*it;
           if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
             CallSite cs(inst);
             if (isa<InlineAsm>(cs.getCalledValue())) {
@@ -721,7 +721,7 @@ void StatsTracker::computeReachableUncovered() {
     std::vector<Instruction *> instructions;
     for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
          fnIt != fn_ie; ++fnIt) {
-      Function *fn = static_cast<Function *>(fnIt);
+      Function *fn = &*fnIt;
       if (fnIt->isDeclaration()) {
         if (fnIt->doesNotReturn()) {
           functionShortestPath[fn] = 0;
@@ -737,7 +737,7 @@ void StatsTracker::computeReachableUncovered() {
            bbIt != bb_ie; ++bbIt) {
         for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
              it != ie; ++it) {
-          Instruction *inst = static_cast<Instruction *>(it);
+          Instruction *inst = &*it;
           instructions.push_back(inst);
           unsigned id = infos.getInfo(inst).id;
           sm.setIndexedValue(stats::minDistToReturn, 
@@ -796,14 +796,13 @@ void StatsTracker::computeReachableUncovered() {
           // functionShortestPath, or it will remain 0 (erroneously indicating
           // that no return instructions are reachable)
           Function *f = inst->getParent()->getParent();
-          if (best != cur
-              || (inst == static_cast<Instruction *>(f->begin()->begin())
+          if (best != cur || (inst == &*(f->begin()->begin())
                   && functionShortestPath[f] != best)) {
             sm.setIndexedValue(stats::minDistToReturn, id, best);
             changed = true;
 
             // Update shortest path if this is the entry point.
-            if (inst == static_cast<Instruction *>(f->begin()->begin()))
+            if (inst == &*(f->begin()->begin()))
               functionShortestPath[f] = best;
           }
         }
@@ -820,7 +819,7 @@ void StatsTracker::computeReachableUncovered() {
          bbIt != bb_ie; ++bbIt) {
       for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
            it != ie; ++it) {
-        Instruction *inst = static_cast<Instruction *>(it);
+        Instruction *inst = &*it;
         unsigned id = infos.getInfo(inst).id;
         instructions.push_back(inst);
         sm.setIndexedValue(stats::minDistToUncovered, 
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index b70bcbef..3b66f641 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -13,12 +13,10 @@
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
-#include "klee/Internal/System/Time.h"
+#include "klee/TimerStatIncrementer.h"
 
 #include "CoreStats.h"
 
-#include "llvm/Support/TimeValue.h"
-
 using namespace klee;
 using namespace llvm;
 
@@ -32,17 +30,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -55,17 +50,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -101,17 +93,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
   
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -125,16 +114,13 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   if (objects.empty())
     return true;
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   bool success = solver->getInitialValues(Query(state.constraints,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  state.queryCost += timer.check() / 1e6;
   
   return success;
 }
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 48a4eb94..eb0f189b 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -71,7 +71,7 @@ bool DivCheckPass::runOnModule(Module &M) {
                                           Type::getInt64Ty(ctx),
                                           false,  /* sign doesn't matter */
                                           "int_cast_to_i64",
-                                          static_cast<Instruction *>(i));
+                                          &*i);
             
             // Lazily bind the function to avoid always importing it.
             if (!divZeroCheckFunction) {
@@ -129,7 +129,7 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
                                           Type::getInt64Ty(ctx),
                                           false,  /* sign doesn't matter */
                                           "int_cast_to_i64",
-                                          static_cast<Instruction *>(i));
+                                          &*i);
             args.push_back(shift);
 
 
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 8f6c7c2b..3ba4895e 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -120,7 +120,7 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
 
   for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
        fnIt != fn_ie; ++fnIt) {
-    Function *fn = static_cast<Function *>(fnIt);
+    Function *fn = &*fnIt;
 
     // We want to ensure that as all instructions have source information, if
     // available. Clang sometimes will not write out debug information on the
@@ -193,6 +193,6 @@ InstructionInfoTable::getFunctionInfo(const Function *f) const {
     // and construct a test case for it if it does, though.
     return dummyInfo;
   } else {
-    return getInfo(static_cast<const Instruction *>(f->begin()->begin()));
+    return getInfo(&*(f->begin()->begin()));
   }
 }
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 215b2275..ec9972eb 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -196,7 +196,7 @@ static void injectStaticConstructorsAndDestructors(Module *m) {
 
     if (ctors)
     CallInst::Create(getStubFunctionForCtorList(m, ctors, "klee.ctor_stub"),
-		     "", static_cast<Instruction *>(mainFn->begin()->begin()));
+		     "", &*(mainFn->begin()->begin()));
     if (dtors) {
       Function *dtorStub = getStubFunctionForCtorList(m, dtors, "klee.dtor_stub");
       for (Function::iterator it = mainFn->begin(), ie = mainFn->end();
@@ -286,7 +286,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
       llvm::errs() << "KLEE: adding klee_merge at exit of: " << name << "\n";
       for (llvm::Function::iterator bbit = f->begin(), bbie = f->end(); 
            bbit != bbie; ++bbit) {
-	BasicBlock *bb = static_cast<BasicBlock *>(bbit);
+	BasicBlock *bb = &*bbit;
         if (bb != exit) {
           Instruction *i = bbit->getTerminator();
           if (i->getOpcode()==Instruction::Ret) {
@@ -470,7 +470,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     if (it->isDeclaration())
       continue;
 
-    Function *fn = static_cast<Function *>(it);
+    Function *fn = &*it;
     KFunction *kf = new KFunction(fn, this);
     
     for (unsigned i=0; i<kf->numInstructions; ++i) {
@@ -561,7 +561,7 @@ KFunction::KFunction(llvm::Function *_function,
     trackCoverage(true) {
   for (llvm::Function::iterator bbit = function->begin(), 
          bbie = function->end(); bbit != bbie; ++bbit) {
-    BasicBlock *bb = static_cast<BasicBlock *>(bbit);
+    BasicBlock *bb = &*bbit;
     basicBlockEntry[bb] = numInstructions;
     numInstructions += bb->size();
   }
@@ -576,7 +576,7 @@ KFunction::KFunction(llvm::Function *_function,
          bbie = function->end(); bbit != bbie; ++bbit) {
     for (llvm::BasicBlock::iterator it = bbit->begin(), ie = bbit->end();
          it != ie; ++it)
-      registerMap[static_cast<Instruction *>(it)] = rnum++;
+      registerMap[&*it] = rnum++;
   }
   numRegisters = rnum;
   
@@ -596,7 +596,7 @@ KFunction::KFunction(llvm::Function *_function,
         ki = new KInstruction(); break;
       }
 
-      Instruction *inst = static_cast<Instruction *>(it);
+      Instruction *inst = &*it;
       ki->inst = inst;
       ki->dest = registerMap[inst];
 
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 5cc6b991..b20c21ab 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -44,7 +44,7 @@ bool LowerSwitchPass::runOnFunction(Function &F) {
   bool changed = false;
 
   for (Function::iterator I = F.begin(), E = F.end(); I != E; ) {
-    BasicBlock *cur = static_cast<BasicBlock *>(I);
+    BasicBlock *cur = &*I;
     I++; // Advance over block so we don't traverse new blocks
 
     if (SwitchInst *SI = dyn_cast<SwitchInst>(cur->getTerminator())) {
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index 5fc54ef1..113dcc62 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -124,7 +124,7 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) {
     for (Function::iterator bi = fi->begin(), be = fi->end(); bi != be; ++bi) {
       for (BasicBlock::iterator ii = bi->begin(), ie = bi->end(); ii != ie;) {
-        Instruction *i = static_cast<Instruction *>(ii);
+        Instruction *i = &*ii;
         ++ii;  
         changed |= runOnInstruction(M, i);
       }
diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h
index 8dc97e06..105c7c75 100644
--- a/lib/Solver/Z3Solver.h
+++ b/lib/Solver/Z3Solver.h
@@ -14,7 +14,7 @@
 #include "klee/Solver.h"
 
 namespace klee {
-/// Z3Solver - A solver complete solver based on Z3
+/// Z3Solver - A complete solver based on Z3
 class Z3Solver : public Solver {
 public:
   /// Z3Solver - Construct a new Z3Solver.
diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp
index ef59b2a9..a0e1596f 100644
--- a/lib/Support/TreeStream.cpp
+++ b/lib/Support/TreeStream.cpp
@@ -63,7 +63,6 @@ TreeOStream TreeStreamWriter::open(const TreeOStream &os) {
 }
 
 void TreeStreamWriter::write(TreeOStream &os, const char *s, unsigned size) {
-#if 1
   if (bufferCount && 
       (os.id!=lastID || size+bufferCount>bufferSize))
     flushBuffer();
@@ -77,13 +76,8 @@ void TreeStreamWriter::write(TreeOStream &os, const char *s, unsigned size) {
   } else {
     output->write(reinterpret_cast<const char*>(&os.id), 4);
     output->write(reinterpret_cast<const char*>(&size), 4);
-    output->write(buffer, size);
+    output->write(s, size);
   }
-#else
-  output->write(reinterpret_cast<const char*>(&os.id), 4);
-  output->write(reinterpret_cast<const char*>(&size), 4);
-  output->write(s, size);
-#endif
 }
 
 void TreeStreamWriter::flushBuffer() {
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 3662cbee..d04963e1 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -668,10 +668,10 @@ static int initEnv(Module *mainModule) {
     klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n");
   }
 
-  Instruction *firstInst = static_cast<Instruction *>(mainFn->begin()->begin());
+  Instruction *firstInst = &*(mainFn->begin()->begin());
 
-  Value *oldArgc = static_cast<Argument *>(mainFn->arg_begin());
-  Value *oldArgv = static_cast<Argument *>(++mainFn->arg_begin());
+  Value *oldArgc = &*(mainFn->arg_begin());
+  Value *oldArgv = &*(++mainFn->arg_begin());
 
   AllocaInst* argcPtr =
     new AllocaInst(oldArgc->getType(), "argcPtr", firstInst);
@@ -1078,7 +1078,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   // naming conflict.
   for (Module::iterator fi = mainModule->begin(), fe = mainModule->end();
        fi != fe; ++fi) {
-    Function *f = static_cast<Function *>(fi);
+    Function *f = &*fi;
     const std::string &name = f->getName();
     if (name[0]=='\01') {
       unsigned size = name.size();
@@ -1137,8 +1137,8 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   std::vector<llvm::Value*> args;
   args.push_back(llvm::ConstantExpr::getBitCast(userMainFn,
                                                 ft->getParamType(0)));
-  args.push_back(static_cast<Argument *>(stub->arg_begin())); // argc
-  args.push_back(static_cast<Argument *>(++stub->arg_begin())); // argv
+  args.push_back(&*(stub->arg_begin())); // argc
+  args.push_back(&*(++stub->arg_begin())); // argv
   args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init
   args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini
   args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
index a85c0a74..85b7b061 100644
--- a/unittests/CMakeLists.txt
+++ b/unittests/CMakeLists.txt
@@ -79,6 +79,7 @@ add_subdirectory(Assignment)
 add_subdirectory(Expr)
 add_subdirectory(Ref)
 add_subdirectory(Solver)
+add_subdirectory(TreeStream)
 
 # Set up lit configuration
 set (UNIT_TEST_EXE_SUFFIX "Test")
diff --git a/unittests/Makefile b/unittests/Makefile
index 2a73b809..582b8d8d 100644
--- a/unittests/Makefile
+++ b/unittests/Makefile
@@ -17,7 +17,7 @@ CPP.Flags += -I$(LLVM_SRC_ROOT)/utils/unittest/googletest/include/
 CPP.Flags += -Wno-variadic-macros
 
 # FIXME: Parallel dirs is broken?
-DIRS = Expr Solver Ref Assignment
+DIRS = Expr Solver Ref Assignment TreeStream
 
 include $(LEVEL)/Makefile.common
 
diff --git a/unittests/TreeStream/CMakeLists.txt b/unittests/TreeStream/CMakeLists.txt
new file mode 100644
index 00000000..4b298724
--- /dev/null
+++ b/unittests/TreeStream/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_klee_unit_test(TreeStreamTest
+  TreeStreamTest.cpp)
+target_link_libraries(TreeStreamTest PRIVATE kleeBasic)
diff --git a/unittests/TreeStream/Makefile b/unittests/TreeStream/Makefile
new file mode 100644
index 00000000..a56659b9
--- /dev/null
+++ b/unittests/TreeStream/Makefile
@@ -0,0 +1,11 @@
+##===- unittests/Expr/Makefile -----------------------------*- Makefile -*-===##
+
+LEVEL := ../..
+include $(LEVEL)/Makefile.config
+
+TESTNAME := TreeStreamTest
+USEDLIBS := kleeBasic.a kleeSupport.a
+LINK_COMPONENTS := support
+
+include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
+
diff --git a/unittests/TreeStream/TreeStreamTest.cpp b/unittests/TreeStream/TreeStreamTest.cpp
new file mode 100644
index 00000000..09d62c6e
--- /dev/null
+++ b/unittests/TreeStream/TreeStreamTest.cpp
@@ -0,0 +1,48 @@
+#include "klee/Internal/ADT/TreeStream.h"
+#include <vector>
+#include <cstring>
+
+#include "gtest/gtest.h"
+
+using namespace klee;
+
+/* Basic test, checking that after writing "abc" and then "defg", we
+   get a {'a', 'b', 'c', 'c', 'd', 'e', 'f', 'g' } back.  */
+TEST(TreeStreamTest, Basic) {
+  TreeStreamWriter tsw("tsw1.out");
+  ASSERT_TRUE(tsw.good());
+  
+  TreeOStream tos = tsw.open();
+  tos.write("abc", 3);
+  tos.write("defg", 4);
+  tos.flush();
+
+  std::vector<unsigned char> out;
+  tsw.readStream(tos.getID(), out);
+  ASSERT_EQ(out.size(), 7);
+  
+  for (unsigned char c = 'a'; c <= 'g'; c++)
+    ASSERT_EQ(out[c - 'a'], c);
+}
+
+
+/* This tests the case when we perform a write with a size larger than
+   the buffer size, which is a constant set to 4*4096.  This test fails 
+   without #704 */
+TEST(TreeStreamTest, WriteLargerThanBufferSize) {
+  TreeStreamWriter tsw("tsw2.out");
+  ASSERT_TRUE(tsw.good());
+  
+  TreeOStream tos = tsw.open();
+#define NBYTES 5*4096
+  char buf[NBYTES];
+  memset(buf, 'A', sizeof(buf));
+  tos.write(buf, NBYTES);
+  tos.flush();
+
+  std::vector<unsigned char> out;
+  tsw.readStream(tos.getID(), out);
+  ASSERT_EQ(out.size(), NBYTES);
+  for (unsigned i=0; i<out.size(); i++)
+    ASSERT_EQ('A', out[i]);
+}