From 266cc79f26aa8df4718f2309808f77a5426f266c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 23 May 2009 02:42:09 +0000 Subject: 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 --- lib/Core/Executor.cpp | 8 ++++---- lib/Core/Executor.h | 10 +++++----- lib/Core/SeedInfo.cpp | 8 ++++---- lib/Core/SeedInfo.h | 12 ++++++------ 4 files changed, 19 insertions(+), 19 deletions(-) (limited to 'lib/Core') 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 &v = seedMap[&initialState]; - for (std::vector::const_iterator it = usingSeeds->begin(), + for (std::vector::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::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 #include -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 *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 *usingSeeds; + const std::vector *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 *seeds) { + virtual void useSeeds(const std::vector *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; inumObjects; ++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 (inumObjects) { - 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 used; + std::set 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 -- cgit 1.4.1