about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Internal/ADT/KTest.h (renamed from include/klee/Internal/ADT/BOut.h)32
-rw-r--r--include/klee/Interpreter.h6
-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
-rw-r--r--runtime/Runtest/intrinsics.c16
-rw-r--r--test/Feature/DumpStatesOnHalt.c2
-rw-r--r--test/Feature/InAndOutOfBounds.c2
-rw-r--r--test/Feature/LowerSwitch.c4
-rw-r--r--test/Feature/MultipleFreeResolution.c2
-rw-r--r--test/Feature/NamedSeedMatching.c6
-rw-r--r--test/Feature/OverlappedError.c2
-rw-r--r--test/Feature/PreferCex.c2
-rw-r--r--test/regression/2007-10-12-failed-make-symbolic-after-copy.c2
-rw-r--r--tools/gen-random-bout/gen-random-bout.cpp16
-rw-r--r--tools/klee/main.cpp38
-rw-r--r--www/tutorial-1.html36
19 files changed, 130 insertions, 128 deletions
diff --git a/include/klee/Internal/ADT/BOut.h b/include/klee/Internal/ADT/KTest.h
index 14aeb714..c6586f9e 100644
--- a/include/klee/Internal/ADT/BOut.h
+++ b/include/klee/Internal/ADT/KTest.h
@@ -1,4 +1,4 @@
-//===-- BOut.h --------------------------------------------------*- C++ -*-===//
+//===-- KTest.h --------------------------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,23 +7,23 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef __COMMON_BOUT_H__
-#define __COMMON_BOUT_H__
+#ifndef __COMMON_KTEST_H__
+#define __COMMON_KTEST_H__
 
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-  typedef struct BOutObject BOutObject;
-  struct BOutObject {
+  typedef struct KTestObject KTestObject;
+  struct KTestObject {
     char *name;
     unsigned numBytes;
     unsigned char *bytes;
   };
   
-  typedef struct BOut BOut;
-  struct BOut {
+  typedef struct KTest KTest;
+  struct KTest {
     /* file format version */
     unsigned version; 
     
@@ -34,26 +34,26 @@ extern "C" {
     unsigned symArgvLen;
 
     unsigned numObjects;
-    BOutObject *objects;
+    KTestObject *objects;
   };
 
   
-  /* returns the current .bout file format version */
-  unsigned bOut_getCurrentVersion();
+  /* returns the current .ktest file format version */
+  unsigned kTest_getCurrentVersion();
   
-  /* return true iff file at path matches BOut header */
-  int   bOut_isBOutFile(const char *path);
+  /* return true iff file at path matches KTest header */
+  int   kTest_isKTestFile(const char *path);
 
   /* returns NULL on (unspecified) error */
-  BOut* bOut_fromFile(const char *path);
+  KTest* kTest_fromFile(const char *path);
 
   /* returns 1 on success, 0 on (unspecified) error */
-  int   bOut_toFile(BOut *, const char *path);
+  int   kTest_toFile(KTest *, const char *path);
   
   /* returns total number of object bytes */
-  unsigned bOut_numBytes(BOut *);
+  unsigned kTest_numBytes(KTest *);
 
-  void  bOut_free(BOut *);
+  void  kTest_free(KTest *);
 
 #ifdef __cplusplus
 }
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index eca6e59e..14e653c1 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -14,7 +14,7 @@
 #include <map>
 #include <set>
 
-struct BOut;
+struct KTest;
 
 namespace llvm {
 class Function;
@@ -102,7 +102,7 @@ public:
 
   // supply a test case to replay from. this can be used to drive the
   // interpretation down a user specified path. use null to reset.
-  virtual void setReplayOut(const struct BOut *out) = 0;
+  virtual void setReplayOut(const struct KTest *out) = 0;
 
   // supply a list of branch decisions specifying which direction to
   // take on forks. this can be used to drive the interpretation down
@@ -111,7 +111,7 @@ public:
 
   // supply a set of symbolic bindings that will be used as "seeds"
   // for the search. use null to reset.
-  virtual void useSeeds(const std::vector<struct BOut *> *seeds) = 0;
+  virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
 
   virtual void runFunctionAsMain(llvm::Function *f,
                                  int argc,
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
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 36efb5c2..bcd072ac 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -19,9 +19,9 @@
 
 #include "klee/klee.h"
 
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 
-static BOut *testData = 0;
+static KTest *testData = 0;
 static unsigned testPosition = 0;
 
 static unsigned char rand_byte(void) {
@@ -61,21 +61,21 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
 
   if (!testData) {
     char tmp[256];
-    char *name = getenv("KLEE_RUNTEST");
+    char *name = getenv("KTEST_FILE");
 
     if (!name) {
-      fprintf(stdout, "KLEE-RUNTIME: KLEE_RUNTEST not set, please enter .bout path: ");
+      fprintf(stdout, "KLEE-RUNTIME: KTEST_FILE not set, please enter .ktest path: ");
       fflush(stdout);
       name = tmp;
       if (!fgets(tmp, sizeof tmp, stdin) || !strlen(tmp)) {
-        fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KLEE_RUNTEST or user input\n");
+        fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KTEST_FILE or user input\n");
         exit(1);
       }
       tmp[strlen(tmp)-1] = '\0'; /* kill newline */
     }
-    testData = bOut_fromFile(name);
+    testData = kTest_fromFile(name);
     if (!testData) {
-      fprintf(stderr, "KLEE-RUNTIME: unable to open .bout file\n");
+      fprintf(stderr, "KLEE-RUNTIME: unable to open .ktest file\n");
       exit(1);
     }
   }
@@ -84,7 +84,7 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
     fprintf(stderr, "ERROR: out of inputs, using zero\n");
     memset(array, 0, nbytes);
   } else {
-    BOutObject *o = &testData->objects[testPosition++];
+    KTestObject *o = &testData->objects[testPosition++];
     memcpy(array, o->bytes, nbytes<o->numBytes ? nbytes : o->numBytes);
     if (nbytes != o->numBytes) {
       fprintf(stderr, "ERROR: object sizes differ\n");
diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c
index 7e9cf46a..d86b786b 100644
--- a/test/Feature/DumpStatesOnHalt.c
+++ b/test/Feature/DumpStatesOnHalt.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc
-// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000001.ktest
 
 int main() {
   int x = 10;
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index 18e5d2b2..ba655b83 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -2,7 +2,7 @@
 // RUN: %klee %t1.bc
 // RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err 
 // RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err 
-// RUN: test ! -f klee-last/test000003.bout
+// RUN: test ! -f klee-last/test000003.ktest
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
index c4d9644a..1b92e398 100644
--- a/test/Feature/LowerSwitch.c
+++ b/test/Feature/LowerSwitch.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
-// RUN: not test -f klee-last/test000010.bout
+// RUN: not test -f klee-last/test000010.ktest
 // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
-// RUN: test -f klee-last/test000010.bout
+// RUN: test -f klee-last/test000010.ktest
 
 #include <stdio.h>
 
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
index 872d6856..8a36f459 100644
--- a/test/Feature/MultipleFreeResolution.c
+++ b/test/Feature/MultipleFreeResolution.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --emit-all-errors %t1.bc
-// RUN: ls klee-last/ | grep .out | wc -l | grep 4
+// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
 // RUN: ls klee-last/ | grep .err | wc -l | grep 3
 
 #include <stdlib.h>
diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c
index cff34282..bb7f6097 100644
--- a/test/Feature/NamedSeedMatching.c
+++ b/test/Feature/NamedSeedMatching.c
@@ -1,9 +1,9 @@
 // RUN: %llvmgcc -c -g %s -o %t.bc
 // RUN: rm -rf %t.out
 // RUN: %klee --output-dir=%t.out %t.bc "initial"
-// RUN: test -f %t.out/test000001.bout
-// RUN: not test -f %t.out/test000002.bout
-// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.bout %t.bc > %t.log
+// RUN: test -f %t.out/test000001.ktest
+// RUN: not test -f %t.out/test000002.ktest
+// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.ktest %t.bc > %t.log
 // RUN: grep -q "a==3" %t.log
 // RUN: grep -q "b==4" %t.log
 // RUN: grep -q "c==5" %t.log
diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c
index 3c79380c..aa220ed9 100644
--- a/test/Feature/OverlappedError.c
+++ b/test/Feature/OverlappedError.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: ls klee-last/ | grep .out | wc -l | grep 4
+// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4
 // RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
 
 #include <stdlib.h>
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index d73b6076..97ce5101 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
-// RUN: klee-bout-tool klee-last/test000001.bout | grep -F 'Hi\x00\x00'
+// RUN: ktest-tool klee-last/test000001.ktest | grep -F 'Hi\x00\x00'
 
 #include <assert.h>
 #include <stdlib.h>
diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
index 9d81fad0..e9a280c3 100644
--- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
+++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee %t1.bc
-// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000001.ktest
 
 int main() {
   unsigned x, y[4];
diff --git a/tools/gen-random-bout/gen-random-bout.cpp b/tools/gen-random-bout/gen-random-bout.cpp
index 044c3d24..0a65bda2 100644
--- a/tools/gen-random-bout/gen-random-bout.cpp
+++ b/tools/gen-random-bout/gen-random-bout.cpp
@@ -7,7 +7,7 @@
 #include <time.h>
 #include <unistd.h>
 
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 
 // --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
 static int getint(char *i) {
@@ -19,9 +19,9 @@ static int getint(char *i) {
 }
 
 #define MAX 64
-static void push_obj(BOut *b, const char *name, unsigned non_zero_bytes, 
+static void push_obj(KTest *b, const char *name, unsigned non_zero_bytes, 
                      unsigned total_bytes) {
-  BOutObject *o = &b->objects[b->numObjects++];
+  KTestObject *o = &b->objects[b->numObjects++];
   assert(b->numObjects < MAX);
 
   o->name = strdup(name);
@@ -37,8 +37,8 @@ static void push_obj(BOut *b, const char *name, unsigned non_zero_bytes,
 }
 
 
-static void push_range(BOut *b, const char *name, unsigned value) {
-  BOutObject *o = &b->objects[b->numObjects++];
+static void push_range(KTest *b, const char *name, unsigned value) {
+  KTestObject *o = &b->objects[b->numObjects++];
   assert(b->numObjects < MAX);
 
   o->name = strdup(name);
@@ -65,14 +65,14 @@ int main(int argc, char *argv[]) {
     srandom(seed);
   else srandom(time(NULL) * getpid());
 
-  BOut b;
+  KTest b;
   b.numArgs = argc;
   b.args = argv;
   b.symArgvs = 0;
   b.symArgvLen = 0;
 
   b.numObjects = 0;
-  b.objects = (BOutObject *)malloc(MAX * sizeof *b.objects);
+  b.objects = (KTestObject *)malloc(MAX * sizeof *b.objects);
 
   for(i = 2; i < (unsigned)argc; i++) {
     if(strcmp(argv[i], "--sym-args") == 0) {
@@ -118,7 +118,7 @@ int main(int argc, char *argv[]) {
     }
   }
 
-  if (!bOut_toFile(&b, "file.bout"))
+  if (!kTest_toFile(&b, "file.bout"))
     assert(0);
   return 0;
 }
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 0a070452..97911759 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -8,7 +8,7 @@
 #include "klee/Interpreter.h"
 #include "klee/Statistics.h"
 #include "klee/Config/config.h"
-#include "klee/Internal/ADT/BOut.h"
+#include "klee/Internal/ADT/KTest.h"
 #include "klee/Internal/ADT/TreeStream.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
@@ -385,16 +385,16 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     unsigned id = ++m_testIndex;
 
     if (success) {
-      BOut b;      
+      KTest b;      
       b.numArgs = m_argc;
       b.args = m_argv;
       b.symArgvs = 0;
       b.symArgvLen = 0;
       b.numObjects = out.size();
-      b.objects = new BOutObject[b.numObjects];
+      b.objects = new KTestObject[b.numObjects];
       assert(b.objects);
       for (unsigned i=0; i<b.numObjects; i++) {
-        BOutObject *o = &b.objects[i];
+        KTestObject *o = &b.objects[i];
         o->name = const_cast<char*>(out[i].first.c_str());
         o->numBytes = out[i].second.size();
         o->bytes = new unsigned char[o->numBytes];
@@ -402,7 +402,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
         std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
       }
       
-      if (!bOut_toFile(&b, getTestFilename("bout", id).c_str())) {
+      if (!kTest_toFile(&b, getTestFilename("ktest", id).c_str())) {
         klee_warning("unable to write output test case, losing it");
       }
       
@@ -1274,13 +1274,13 @@ int main(int argc, char **argv, char **envp) {
            it = ReplayOutDir.begin(), ie = ReplayOutDir.end();
          it != ie; ++it)
       KleeHandler::getOutFiles(*it, outFiles);    
-    std::vector<BOut*> bOuts;
+    std::vector<KTest*> kTests;
     for (std::vector<std::string>::iterator
            it = outFiles.begin(), ie = outFiles.end();
          it != ie; ++it) {
-      BOut *out = bOut_fromFile(it->c_str());
+      KTest *out = kTest_fromFile(it->c_str());
       if (out) {
-        bOuts.push_back(out);
+        kTests.push_back(out);
       } else {
         llvm::cerr << "KLEE: unable to open: " << *it << "\n";
       }
@@ -1294,28 +1294,28 @@ int main(int argc, char **argv, char **envp) {
     }
 
     unsigned i=0;
-    for (std::vector<BOut*>::iterator
-           it = bOuts.begin(), ie = bOuts.end();
+    for (std::vector<KTest*>::iterator
+           it = kTests.begin(), ie = kTests.end();
          it != ie; ++it) {
-      BOut *out = *it;
+      KTest *out = *it;
       interpreter->setReplayOut(out);
-      llvm::cerr << "KLEE: replaying: " << *it << " (" << bOut_numBytes(out) << " bytes)"
+      llvm::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)"
                  << " (" << ++i << "/" << outFiles.size() << ")\n";
       // XXX should put envp in .bout ?
       interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
       if (interrupted) break;
     }
     interpreter->setReplayOut(0);
-    while (!bOuts.empty()) {
-      bOut_free(bOuts.back());
-      bOuts.pop_back();
+    while (!kTests.empty()) {
+      kTest_free(kTests.back());
+      kTests.pop_back();
     }
   } else {
-    std::vector<BOut *> seeds;
+    std::vector<KTest *> seeds;
     for (std::vector<std::string>::iterator
            it = SeedOutFile.begin(), ie = SeedOutFile.end();
          it != ie; ++it) {
-      BOut *out = bOut_fromFile(it->c_str());
+      KTest *out = kTest_fromFile(it->c_str());
       if (!out) {
         llvm::cerr << "KLEE: unable to open: " << *it << "\n";
         exit(1);
@@ -1330,7 +1330,7 @@ int main(int argc, char **argv, char **envp) {
       for (std::vector<std::string>::iterator
              it2 = outFiles.begin(), ie = outFiles.end();
            it2 != ie; ++it2) {
-        BOut *out = bOut_fromFile(it2->c_str());
+        KTest *out = kTest_fromFile(it2->c_str());
         if (!out) {
           llvm::cerr << "KLEE: unable to open: " << *it2 << "\n";
           exit(1);
@@ -1356,7 +1356,7 @@ int main(int argc, char **argv, char **envp) {
     interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
 
     while (!seeds.empty()) {
-      bOut_free(seeds.back());
+      kTest_free(seeds.back());
       seeds.pop_back();
     }
   }
diff --git a/www/tutorial-1.html b/www/tutorial-1.html
index 389359b2..9f458237 100644
--- a/www/tutorial-1.html
+++ b/www/tutorial-1.html
@@ -101,33 +101,34 @@
 
   <pre class="output">
   $ ls klee-last/
-  assembly.ll  messages.txt  run.stats        test000002.bout  warnings.txt 
-  info         run.istats    test000001.bout  test000003.bout  </pre>
+  assembly.ll      run.istats       test000002.ktest
+  info             run.stats        test000003.ktest
+  messages.txt     test000001.ktest warnings.txt </pre>
 
   Please click <a href="klee-files.html">here</a> if you would like an
   overview of the files generated by KLEE.  In this tutorial, we only
   focus on the actual test files generated by KLEE.
 
   <h2>KLEE-generated test cases</h2> The test cases generated by KLEE
-  are written in files with extension <tt>.bout</tt>.  These are
-  binary files, which can be read with the <tt>klee-bout-tool</tt>
+  are written in files with extension <tt>.ktest</tt>.  These are
+  binary files, which can be read with the <tt>ktest-tool</tt>
   utility.  So let's examine each file:
 
   <pre class="output">
-  $ klee-bout-tool klee-last/test000001.bout 
-  bout file  : 'klee-last/test000001.bout'
+  $ ktest-tool klee-last/test000001.ktest 
+  bout file  : 'klee-last/test000001.ktest'
   args       : ['demo.o']
   num objects: 1
   object    0: name: 'input'
   object    0: size: 1
-  object    0: data: 'b' 
+  object    0: data: 'b'
 
-  $ klee-bout-tool klee-last/test000002.bout 
+  $ ktest-tool klee-last/test000002.ktest 
   ...
   object    0: data: '~'
- 
-  $ klee-bout-tool klee-last/test000003.bout 
-  ...
+
+  $ ktest-tool klee-last/test000003.ktest 
+  ..
   object    0: data: '\x00' </pre>
 
   In each test file, KLEE reports the arguments with which the program
@@ -150,21 +151,22 @@
   hand, (or with the help of an existing test infrastructure), KLEE
   provides a convenient <i>replay library</i>, which simply replaces
   the call to <tt>klee_make_symbolic</tt> with a call to a function
-  that assigns to our input the value stored in the .bout file.
+  that assigns to our input the value stored in the <tt>.ktest</tt>
+  file.
 
   To use it, simply link your program with the <tt>libkleeRuntest</tt>
-  library and set the <tt>KLEE_RUNTEST</tt> environment variable to
+  library and set the <tt>KTEST_FILE</tt> environment variable to
   point to the name of the desired test case:
 
   <pre class="output">
-  $ gcc path/to/klee/Release/lib/libkleeRuntest.dylib demo.c
-  $ KLEE_RUNTEST=klee-last/test000001.bout ./a.out 
+  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
+  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
   $ echo $?
   1
-  $ KLEE_RUNTEST=klee-last/test000002.bout ./a.out 
+  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
   $ echo $?
   0
-  $ KLEE_RUNTEST=klee-last/test000003.bout ./a.out
+  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
   $ echo $?
   0 </pre>
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 01:01:27 +0000