Changed bout to ktest. Kept "BOUT\n" as the header of test files, for backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 19 insertions, 19 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d3409908..df8fdba8 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/Config/config.h"
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
@@ -2227,7 +2227,7 @@ void Executor::run(ExecutionState &initialState) {
   if (usingSeeds) {
     std::vector<SeedInfo> &v = seedMap[&initialState];
     
-    for (std::vector<BOut*>::const_iterator it = usingSeeds->begin(), 
+    for (std::vector<KTest*>::const_iterator it = usingSeeds->begin(), 
            ie = usingSeeds->end(); it != ie; ++it)
       v.push_back(SeedInfo(*it));
 
@@ -2973,7 +2973,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
       for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
              siie = it->second.end(); siit != siie; ++siit) {
         SeedInfo &si = *siit;
-        BOutObject *obj = si.getNextInput(mo,
+        KTestObject *obj = si.getNextInput(mo,
                                           NamedSeedMatching);
 
         if (!obj) {
@@ -3019,7 +3019,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     if (replayPosition >= replayOut->numObjects) {
       terminateStateOnError(state, "replay count mismatch", "user.err");
     } else {
-      BOutObject *obj = &replayOut->objects[replayPosition++];
+      KTestObject *obj = &replayOut->objects[replayPosition++];
       if (obj->numBytes != mo->size) {
         terminateStateOnError(state, "replay size mismatch", "user.err");
       } else {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 76868291..9fa63a04 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -22,7 +22,7 @@
 #include <map>
 #include <set>
 
-struct BOut;
+struct KTest;
 
 namespace llvm {
   class BasicBlock;
@@ -134,7 +134,7 @@ private:
 
   /// When non-null the bindings that will be used for calls to
   /// klee_make_symbolic in order replay.
-  const struct BOut *replayOut;
+  const struct KTest *replayOut;
   /// When non-null a list of branch decisions to be used for replay.
   const std::vector<bool> *replayPath;
   /// The index into the current \ref replayOut or \ref replayPath
@@ -143,7 +143,7 @@ private:
 
   /// When non-null a list of "seed" inputs which will be used to
   /// drive execution.
-  const std::vector<struct BOut *> *usingSeeds;  
+  const std::vector<struct KTest *> *usingSeeds;  
 
   /// Disables forking, instead a random path is chosen. Enabled as
   /// needed to control memory usage. \see fork()
@@ -386,7 +386,7 @@ public:
     symPathWriter = tsw;
   }      
 
-  virtual void setReplayOut(const struct BOut *out) {
+  virtual void setReplayOut(const struct KTest *out) {
     assert(!replayPath && "cannot replay both buffer and path");
     replayOut = out;
     replayPosition = 0;
@@ -401,7 +401,7 @@ public:
   virtual const llvm::Module *
   setModule(llvm::Module *module, const ModuleOptions &opts);
 
-  virtual void useSeeds(const std::vector<struct BOut *> *seeds) { 
+  virtual void useSeeds(const std::vector<struct KTest *> *seeds) { 
     usingSeeds = seeds;
   }
 
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index d76d75dc..e6d88bac 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -16,17 +16,17 @@
 #include "klee/ExecutionState.h"
 #include "klee/Expr.h"
 #include "klee/util/ExprUtil.h"
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 
 using namespace klee;
 
-BOutObject *SeedInfo::getNextInput(const MemoryObject *mo,
+KTestObject *SeedInfo::getNextInput(const MemoryObject *mo,
                                    bool byName) {
   if (byName) {
     unsigned i;
     
     for (i=0; i<input->numObjects; ++i) {
-      BOutObject *obj = &input->objects[i];
+      KTestObject *obj = &input->objects[i];
       if (std::string(obj->name) == mo->name)
         if (used.insert(obj).second)
           return obj;
@@ -38,7 +38,7 @@ BOutObject *SeedInfo::getNextInput(const MemoryObject *mo,
       if (!used.count(&input->objects[i]))
         break;
     if (i<input->numObjects) {
-      BOutObject *obj = &input->objects[i];
+      KTestObject *obj = &input->objects[i];
       if (obj->numBytes == mo->size) {
         used.insert(obj);
         klee_warning_once(mo, "using seed input %s[%d] for: %s (no name match)",
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index dd151ed0..0acb130b 100644
--- a/lib/Core/SeedInfo.h
+++ b/lib/Core/SeedInfo.h
@@ -13,8 +13,8 @@
 #include "klee/util/Assignment.h"
 
 extern "C" {
-  struct BOut;
-  struct BOutObject;
+  struct KTest;
+  struct KTestObject;
 }
 
 namespace klee {
@@ -24,17 +24,17 @@ namespace klee {
   class SeedInfo {
   public:
     Assignment assignment;
-    BOut *input;
+    KTest *input;
     unsigned inputPosition;
-    std::set<struct BOutObject*> used;
+    std::set<struct KTestObject*> used;
     
   public:
     explicit
-    SeedInfo(BOut *_input) : assignment(true),
+    SeedInfo(KTest *_input) : assignment(true),
                              input(_input),
                              inputPosition(0) {}
     
-    BOutObject *getNextInput(const MemoryObject *mo,
+    KTestObject *getNextInput(const MemoryObject *mo,
                              bool byName);
     
     /// Patch the seed so that condition is satisfied while retaining as