[llvm-commits] [klee] r72312 - in /klee/trunk: include/klee/ include/klee/Internal/ADT/ lib/Basic/ lib/Core/ runtime/Runtest/ test/Feature/ test/regression/ tools/gen-random-bout/ tools/klee/ www/

Cristian Cadar cristic at cs.stanford.edu
Fri May 22 19:42:09 PDT 2009


Author: cristic
Date: Fri May 22 21:42:09 2009
New Revision: 72312

URL: http://llvm.org/viewvc/llvm-project?rev=72312&view=rev
Log:
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.


Added:
    klee/trunk/include/klee/Internal/ADT/KTest.h
      - copied, changed from r72305, klee/trunk/include/klee/Internal/ADT/BOut.h
    klee/trunk/lib/Basic/KTest.cpp
      - copied, changed from r72305, klee/trunk/lib/Basic/BOut.cpp
Removed:
    klee/trunk/include/klee/Internal/ADT/BOut.h
    klee/trunk/lib/Basic/BOut.cpp
Modified:
    klee/trunk/include/klee/Interpreter.h
    klee/trunk/lib/Core/Executor.cpp
    klee/trunk/lib/Core/Executor.h
    klee/trunk/lib/Core/SeedInfo.cpp
    klee/trunk/lib/Core/SeedInfo.h
    klee/trunk/runtime/Runtest/intrinsics.c
    klee/trunk/test/Feature/DumpStatesOnHalt.c
    klee/trunk/test/Feature/InAndOutOfBounds.c
    klee/trunk/test/Feature/LowerSwitch.c
    klee/trunk/test/Feature/MultipleFreeResolution.c
    klee/trunk/test/Feature/NamedSeedMatching.c
    klee/trunk/test/Feature/OverlappedError.c
    klee/trunk/test/Feature/PreferCex.c
    klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
    klee/trunk/tools/gen-random-bout/gen-random-bout.cpp
    klee/trunk/tools/klee/main.cpp
    klee/trunk/www/tutorial-1.html

Removed: klee/trunk/include/klee/Internal/ADT/BOut.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Internal/ADT/BOut.h?rev=72311&view=auto

==============================================================================
--- klee/trunk/include/klee/Internal/ADT/BOut.h (original)
+++ klee/trunk/include/klee/Internal/ADT/BOut.h (removed)
@@ -1,62 +0,0 @@
-//===-- BOut.h --------------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef __COMMON_BOUT_H__
-#define __COMMON_BOUT_H__
-
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-  typedef struct BOutObject BOutObject;
-  struct BOutObject {
-    char *name;
-    unsigned numBytes;
-    unsigned char *bytes;
-  };
-  
-  typedef struct BOut BOut;
-  struct BOut {
-    /* file format version */
-    unsigned version; 
-    
-    unsigned numArgs;
-    char **args;
-
-    unsigned symArgvs;
-    unsigned symArgvLen;
-
-    unsigned numObjects;
-    BOutObject *objects;
-  };
-
-  
-  /* returns the current .bout file format version */
-  unsigned bOut_getCurrentVersion();
-  
-  /* return true iff file at path matches BOut header */
-  int   bOut_isBOutFile(const char *path);
-
-  /* returns NULL on (unspecified) error */
-  BOut* bOut_fromFile(const char *path);
-
-  /* returns 1 on success, 0 on (unspecified) error */
-  int   bOut_toFile(BOut *, const char *path);
-  
-  /* returns total number of object bytes */
-  unsigned bOut_numBytes(BOut *);
-
-  void  bOut_free(BOut *);
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif

Copied: klee/trunk/include/klee/Internal/ADT/KTest.h (from r72305, klee/trunk/include/klee/Internal/ADT/BOut.h)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Internal/ADT/KTest.h?p2=klee/trunk/include/klee/Internal/ADT/KTest.h&p1=klee/trunk/include/klee/Internal/ADT/BOut.h&r1=72305&r2=72312&rev=72312&view=diff

==============================================================================
--- klee/trunk/include/klee/Internal/ADT/BOut.h (original)
+++ klee/trunk/include/klee/Internal/ADT/KTest.h Fri May 22 21:42:09 2009
@@ -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 @@
     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
 }

Modified: klee/trunk/include/klee/Interpreter.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Interpreter.h?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/include/klee/Interpreter.h (original)
+++ klee/trunk/include/klee/Interpreter.h Fri May 22 21:42:09 2009
@@ -14,7 +14,7 @@
 #include <map>
 #include <set>
 
-struct BOut;
+struct KTest;
 
 namespace llvm {
 class Function;
@@ -102,7 +102,7 @@
 
   // 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 @@
 
   // 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,

Removed: klee/trunk/lib/Basic/BOut.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Basic/BOut.cpp?rev=72311&view=auto

==============================================================================
--- klee/trunk/lib/Basic/BOut.cpp (original)
+++ klee/trunk/lib/Basic/BOut.cpp (removed)
@@ -1,236 +0,0 @@
-//===-- BOut.c ------------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "klee/Internal/ADT/BOut.h"
-
-#include <stdlib.h>
-#include <string.h>
-#include <stdio.h>
-
-#define BOUT_MAGIC "BOUT\n"
-#define BOUT_MAGIC_SIZE 5
-#define BOUT_VERSION 2
-
-/***/
-
-static int read_uint32(FILE *f, unsigned *value_out) {
-  unsigned char data[4];
-  if (fread(data, 4, 1, f)!=1)
-    return 0;
-  *value_out = (((((data[0]<<8) + data[1])<<8) + data[2])<<8) + data[3];
-  return 1;
-}
-
-static int write_uint32(FILE *f, unsigned value) {
-  unsigned char data[4];
-  data[0] = value>>24;
-  data[1] = value>>16;
-  data[2] = value>> 8;
-  data[3] = value>> 0;
-  return fwrite(data, 1, 4, f)==4;
-}
-
-static int read_string(FILE *f, char **value_out) {
-  unsigned len;
-  if (!read_uint32(f, &len))
-    return 0;
-  *value_out = (char*) malloc(len+1);
-  if (!*value_out)
-    return 0;
-  if (fread(*value_out, len, 1, f)!=1)
-    return 0;
-  (*value_out)[len] = 0;
-  return 1;
-}
-
-static int write_string(FILE *f, const char *value) {
-  unsigned len = strlen(value);
-  if (!write_uint32(f, len))
-    return 0;
-  if (fwrite(value, len, 1, f)!=1)
-    return 0;
-  return 1;
-}
-
-/***/
-
-
-unsigned bOut_getCurrentVersion() {
-  return BOUT_VERSION;
-}
-
-
-static int bOut_checkHeader(FILE *f) {
-  char header[BOUT_MAGIC_SIZE];
-  if (fread(header, BOUT_MAGIC_SIZE, 1, f)!=1)
-    return 0;
-  if (memcmp(header, BOUT_MAGIC, BOUT_MAGIC_SIZE))
-    return 0;
-  return 1;
-}
-
-int bOut_isBOutFile(const char *path) {
-  FILE *f = fopen(path, "rb");
-  int res;
-
-  if (!f)
-    return 0;
-  res = bOut_checkHeader(f);
-  fclose(f);
-  
-  return res;
-}
-
-BOut *bOut_fromFile(const char *path) {
-  FILE *f = fopen(path, "rb");
-  BOut *res = 0;
-  unsigned i, version;
-
-  if (!f) 
-    goto error;
-  if (!bOut_checkHeader(f)) 
-    goto error;
-
-  res = (BOut*) calloc(1, sizeof(*res));
-  if (!res) 
-    goto error;
-
-  if (!read_uint32(f, &version)) 
-    goto error;
-  
-  if (version > bOut_getCurrentVersion())
-    goto error;
-
-  res->version = version;
-
-  if (!read_uint32(f, &res->numArgs)) 
-    goto error;
-  res->args = (char**) calloc(res->numArgs, sizeof(*res->args));
-  if (!res->args) 
-    goto error;
-  
-  for (i=0; i<res->numArgs; i++)
-    if (!read_string(f, &res->args[i]))
-      goto error;
-
-  if (version >= 2) {
-    if (!read_uint32(f, &res->symArgvs)) 
-      goto error;
-    if (!read_uint32(f, &res->symArgvLen)) 
-      goto error;
-  }
-
-  if (!read_uint32(f, &res->numObjects))
-    goto error;
-  res->objects = (BOutObject*) calloc(res->numObjects, sizeof(*res->objects));
-  if (!res->objects)
-    goto error;
-  for (i=0; i<res->numObjects; i++) {
-    BOutObject *o = &res->objects[i];
-    if (!read_string(f, &o->name))
-      goto error;
-    if (!read_uint32(f, &o->numBytes))
-      goto error;
-    o->bytes = (unsigned char*) malloc(o->numBytes);
-    if (fread(o->bytes, o->numBytes, 1, f)!=1)
-      goto error;
-  }
-
-  fclose(f);
-
-  return res;
- error:
-  if (res) {
-    if (res->args) {
-      for (i=0; i<res->numArgs; i++)
-        if (res->args[i])
-          free(res->args[i]);
-      free(res->args);
-    }
-    if (res->objects) {
-      for (i=0; i<res->numObjects; i++) {
-        BOutObject *bo = &res->objects[i];
-        if (bo->name)
-          free(bo->name);
-        if (bo->bytes)
-          free(bo->bytes);
-      }
-      free(res->objects);
-    }
-    free(res);
-  }
-
-  if (f) fclose(f);
-
-  return 0;
-}
-
-int bOut_toFile(BOut *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)
-    goto error;
-  if (!write_uint32(f, BOUT_VERSION))
-    goto error;
-      
-  if (!write_uint32(f, bo->numArgs))
-    goto error;
-  for (i=0; i<bo->numArgs; i++) {
-    if (!write_string(f, bo->args[i]))
-      goto error;
-  }
-
-  if (!write_uint32(f, bo->symArgvs))
-    goto error;
-  if (!write_uint32(f, bo->symArgvLen))
-    goto error;
-  
-  if (!write_uint32(f, bo->numObjects))
-    goto error;
-  for (i=0; i<bo->numObjects; i++) {
-    BOutObject *o = &bo->objects[i];
-    if (!write_string(f, o->name))
-      goto error;
-    if (!write_uint32(f, o->numBytes))
-      goto error;
-    if (fwrite(o->bytes, o->numBytes, 1, f)!=1)
-      goto error;
-  }
-
-  fclose(f);
-
-  return 1;
- error:
-  if (f) fclose(f);
-  
-  return 0;
-}
-
-unsigned bOut_numBytes(BOut *bo) {
-  unsigned i, res = 0;
-  for (i=0; i<bo->numObjects; i++)
-    res += bo->objects[i].numBytes;
-  return res;
-}
-
-void bOut_free(BOut *bo) {
-  unsigned i;
-  for (i=0; i<bo->numArgs; i++)
-    free(bo->args[i]);
-  free(bo->args);
-  for (i=0; i<bo->numObjects; i++) {
-    free(bo->objects[i].name);
-    free(bo->objects[i].bytes);
-  }
-  free(bo->objects);
-  free(bo);
-}

Copied: klee/trunk/lib/Basic/KTest.cpp (from r72305, klee/trunk/lib/Basic/BOut.cpp)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Basic/KTest.cpp?p2=klee/trunk/lib/Basic/KTest.cpp&p1=klee/trunk/lib/Basic/BOut.cpp&r1=72305&r2=72312&rev=72312&view=diff

==============================================================================
--- klee/trunk/lib/Basic/BOut.cpp (original)
+++ klee/trunk/lib/Basic/KTest.cpp Fri May 22 21:42:09 2009
@@ -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 @@
 /***/
 
 
-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 @@
 
   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 @@
     }
     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 @@
   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 @@
   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 @@
   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]);

Modified: klee/trunk/lib/Core/Executor.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Executor.cpp?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/lib/Core/Executor.cpp (original)
+++ klee/trunk/lib/Core/Executor.cpp Fri May 22 21:42:09 2009
@@ -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 @@
   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 @@
       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 @@
     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 {

Modified: klee/trunk/lib/Core/Executor.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Executor.h?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/lib/Core/Executor.h (original)
+++ klee/trunk/lib/Core/Executor.h Fri May 22 21:42:09 2009
@@ -22,7 +22,7 @@
 #include <map>
 #include <set>
 
-struct BOut;
+struct KTest;
 
 namespace llvm {
   class BasicBlock;
@@ -134,7 +134,7 @@
 
   /// 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 @@
 
   /// 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 @@
     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 @@
   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;
   }
 

Modified: klee/trunk/lib/Core/SeedInfo.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/SeedInfo.cpp?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/lib/Core/SeedInfo.cpp (original)
+++ klee/trunk/lib/Core/SeedInfo.cpp Fri May 22 21:42:09 2009
@@ -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 @@
       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)",

Modified: klee/trunk/lib/Core/SeedInfo.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/SeedInfo.h?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/lib/Core/SeedInfo.h (original)
+++ klee/trunk/lib/Core/SeedInfo.h Fri May 22 21:42:09 2009
@@ -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 @@
   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

Modified: klee/trunk/runtime/Runtest/intrinsics.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Runtest/intrinsics.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/runtime/Runtest/intrinsics.c (original)
+++ klee/trunk/runtime/Runtest/intrinsics.c Fri May 22 21:42:09 2009
@@ -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 @@
 
   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 @@
     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");

Modified: klee/trunk/test/Feature/DumpStatesOnHalt.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/DumpStatesOnHalt.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/DumpStatesOnHalt.c (original)
+++ klee/trunk/test/Feature/DumpStatesOnHalt.c Fri May 22 21:42:09 2009
@@ -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;

Modified: klee/trunk/test/Feature/InAndOutOfBounds.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/InAndOutOfBounds.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/InAndOutOfBounds.c (original)
+++ klee/trunk/test/Feature/InAndOutOfBounds.c Fri May 22 21:42:09 2009
@@ -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;

Modified: klee/trunk/test/Feature/LowerSwitch.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/LowerSwitch.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/LowerSwitch.c (original)
+++ klee/trunk/test/Feature/LowerSwitch.c Fri May 22 21:42:09 2009
@@ -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>
 

Modified: klee/trunk/test/Feature/MultipleFreeResolution.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/MultipleFreeResolution.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/MultipleFreeResolution.c (original)
+++ klee/trunk/test/Feature/MultipleFreeResolution.c Fri May 22 21:42:09 2009
@@ -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>

Modified: klee/trunk/test/Feature/NamedSeedMatching.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/NamedSeedMatching.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/NamedSeedMatching.c (original)
+++ klee/trunk/test/Feature/NamedSeedMatching.c Fri May 22 21:42:09 2009
@@ -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

Modified: klee/trunk/test/Feature/OverlappedError.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/OverlappedError.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/OverlappedError.c (original)
+++ klee/trunk/test/Feature/OverlappedError.c Fri May 22 21:42:09 2009
@@ -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>

Modified: klee/trunk/test/Feature/PreferCex.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/PreferCex.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/Feature/PreferCex.c (original)
+++ klee/trunk/test/Feature/PreferCex.c Fri May 22 21:42:09 2009
@@ -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>

Modified: klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c (original)
+++ klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c Fri May 22 21:42:09 2009
@@ -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];

Modified: klee/trunk/tools/gen-random-bout/gen-random-bout.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/tools/gen-random-bout/gen-random-bout.cpp?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/tools/gen-random-bout/gen-random-bout.cpp (original)
+++ klee/trunk/tools/gen-random-bout/gen-random-bout.cpp Fri May 22 21:42:09 2009
@@ -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 @@
 }
 
 #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_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 @@
     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 @@
     }
   }
 
-  if (!bOut_toFile(&b, "file.bout"))
+  if (!kTest_toFile(&b, "file.bout"))
     assert(0);
   return 0;
 }

Modified: klee/trunk/tools/klee/main.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/tools/klee/main.cpp?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/tools/klee/main.cpp (original)
+++ klee/trunk/tools/klee/main.cpp Fri May 22 21:42:09 2009
@@ -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 @@
     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 @@
         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 @@
            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 @@
     }
 
     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 @@
       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 @@
     interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
 
     while (!seeds.empty()) {
-      bOut_free(seeds.back());
+      kTest_free(seeds.back());
       seeds.pop_back();
     }
   }

Modified: klee/trunk/www/tutorial-1.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorial-1.html?rev=72312&r1=72311&r2=72312&view=diff

==============================================================================
--- klee/trunk/www/tutorial-1.html (original)
+++ klee/trunk/www/tutorial-1.html Fri May 22 21:42:09 2009
@@ -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>
 





More information about the llvm-commits mailing list