about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Basic/KTest.cpp (renamed from lib/Basic/BOut.cpp)54
-rw-r--r--lib/Core/Executor.cpp8
-rw-r--r--lib/Core/Executor.h10
-rw-r--r--lib/Core/SeedInfo.cpp8
-rw-r--r--lib/Core/SeedInfo.h12
5 files changed, 46 insertions, 46 deletions
diff --git a/lib/Basic/BOut.cpp b/lib/Basic/KTest.cpp
index 42d17e27..d17916f5 100644
--- a/lib/Basic/BOut.cpp
+++ b/lib/Basic/KTest.cpp
@@ -1,4 +1,4 @@
-//===-- BOut.c ------------------------------------------------------------===//
+//===-- KTest.cpp ---------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,15 +7,15 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 
 #include <stdlib.h>
 #include <string.h>
 #include <stdio.h>
 
-#define BOUT_MAGIC "BOUT\n"
-#define BOUT_MAGIC_SIZE 5
-#define BOUT_VERSION 2
+#define KTEST_MAGIC "BOUT\n"
+#define KTEST_MAGIC_SIZE 5
+#define KTEST_VERSION 2
 
 /***/
 
@@ -61,50 +61,50 @@ static int write_string(FILE *f, const char *value) {
 /***/
 
 
-unsigned bOut_getCurrentVersion() {
-  return BOUT_VERSION;
+unsigned kTest_getCurrentVersion() {
+  return KTEST_VERSION;
 }
 
 
-static int bOut_checkHeader(FILE *f) {
-  char header[BOUT_MAGIC_SIZE];
-  if (fread(header, BOUT_MAGIC_SIZE, 1, f)!=1)
+static int kTest_checkHeader(FILE *f) {
+  char header[KTEST_MAGIC_SIZE];
+  if (fread(header, KTEST_MAGIC_SIZE, 1, f)!=1)
     return 0;
-  if (memcmp(header, BOUT_MAGIC, BOUT_MAGIC_SIZE))
+  if (memcmp(header, KTEST_MAGIC, KTEST_MAGIC_SIZE))
     return 0;
   return 1;
 }
 
-int bOut_isBOutFile(const char *path) {
+int kTest_isKTestFile(const char *path) {
   FILE *f = fopen(path, "rb");
   int res;
 
   if (!f)
     return 0;
-  res = bOut_checkHeader(f);
+  res = kTest_checkHeader(f);
   fclose(f);
   
   return res;
 }
 
-BOut *bOut_fromFile(const char *path) {
+KTest *kTest_fromFile(const char *path) {
   FILE *f = fopen(path, "rb");
-  BOut *res = 0;
+  KTest *res = 0;
   unsigned i, version;
 
   if (!f) 
     goto error;
-  if (!bOut_checkHeader(f)) 
+  if (!kTest_checkHeader(f)) 
     goto error;
 
-  res = (BOut*) calloc(1, sizeof(*res));
+  res = (KTest*) calloc(1, sizeof(*res));
   if (!res) 
     goto error;
 
   if (!read_uint32(f, &version)) 
     goto error;
   
-  if (version > bOut_getCurrentVersion())
+  if (version > kTest_getCurrentVersion())
     goto error;
 
   res->version = version;
@@ -128,11 +128,11 @@ BOut *bOut_fromFile(const char *path) {
 
   if (!read_uint32(f, &res->numObjects))
     goto error;
-  res->objects = (BOutObject*) calloc(res->numObjects, sizeof(*res->objects));
+  res->objects = (KTestObject*) calloc(res->numObjects, sizeof(*res->objects));
   if (!res->objects)
     goto error;
   for (i=0; i<res->numObjects; i++) {
-    BOutObject *o = &res->objects[i];
+    KTestObject *o = &res->objects[i];
     if (!read_string(f, &o->name))
       goto error;
     if (!read_uint32(f, &o->numBytes))
@@ -155,7 +155,7 @@ BOut *bOut_fromFile(const char *path) {
     }
     if (res->objects) {
       for (i=0; i<res->numObjects; i++) {
-        BOutObject *bo = &res->objects[i];
+        KTestObject *bo = &res->objects[i];
         if (bo->name)
           free(bo->name);
         if (bo->bytes)
@@ -171,15 +171,15 @@ BOut *bOut_fromFile(const char *path) {
   return 0;
 }
 
-int bOut_toFile(BOut *bo, const char *path) {
+int kTest_toFile(KTest *bo, const char *path) {
   FILE *f = fopen(path, "wb");
   unsigned i;
 
   if (!f) 
     goto error;
-  if (fwrite(BOUT_MAGIC, strlen(BOUT_MAGIC), 1, f)!=1)
+  if (fwrite(KTEST_MAGIC, strlen(KTEST_MAGIC), 1, f)!=1)
     goto error;
-  if (!write_uint32(f, BOUT_VERSION))
+  if (!write_uint32(f, KTEST_VERSION))
     goto error;
       
   if (!write_uint32(f, bo->numArgs))
@@ -197,7 +197,7 @@ int bOut_toFile(BOut *bo, const char *path) {
   if (!write_uint32(f, bo->numObjects))
     goto error;
   for (i=0; i<bo->numObjects; i++) {
-    BOutObject *o = &bo->objects[i];
+    KTestObject *o = &bo->objects[i];
     if (!write_string(f, o->name))
       goto error;
     if (!write_uint32(f, o->numBytes))
@@ -215,14 +215,14 @@ int bOut_toFile(BOut *bo, const char *path) {
   return 0;
 }
 
-unsigned bOut_numBytes(BOut *bo) {
+unsigned kTest_numBytes(KTest *bo) {
   unsigned i, res = 0;
   for (i=0; i<bo->numObjects; i++)
     res += bo->objects[i].numBytes;
   return res;
 }
 
-void bOut_free(BOut *bo) {
+void kTest_free(KTest *bo) {
   unsigned i;
   for (i=0; i<bo->numArgs; i++)
     free(bo->args[i]);
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