diff options
author | Daniel Dunbar <daniel@zuster.org> | 2010-03-14 05:08:45 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2010-03-14 05:08:45 +0000 |
commit | 5099d8124393dcd577c2dd091834a17fe2d9fcdb (patch) | |
tree | 5ece7d73b60c043f8ab4e92a3528e1387cbdfcac /include | |
parent | 1efb4b23232930a80cfe7b5a849e42b9919f3ad6 (diff) | |
download | klee-5099d8124393dcd577c2dd091834a17fe2d9fcdb.tar.gz |
Kill off ExecutionTrace stuff, it is too messy.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@98466 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/ExecutionState.h | 105 |
1 files changed, 0 insertions, 105 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 54915843..09999110 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -31,7 +31,6 @@ namespace klee { class MemoryObject; class PTreeNode; class InstructionInfo; - class ExecutionTraceEvent; std::ostream &operator<<(std::ostream &os, const MemoryMap &mm); @@ -62,32 +61,6 @@ struct StackFrame { ~StackFrame(); }; -// FIXME: Redo execution trace stuff to use a TreeStream, there is no -// need to keep this stuff in memory as far as I can tell. - -// each state should have only one of these guys ... -class ExecutionTraceManager { -public: - ExecutionTraceManager() : hasSeenUserMain(false) {} - - void addEvent(ExecutionTraceEvent* evt); - void printAllEvents(std::ostream &os) const; - -private: - // have we seen a call to __user_main() yet? - // don't bother tracing anything until we see this, - // or else we'll get junky prologue shit - bool hasSeenUserMain; - - // ugh C++ only supports polymorphic calls thru pointers - // - // WARNING: these are NEVER FREED, because they are shared - // across different states (when states fork), so we have - // an *intentional* memory leak, but oh wellz ;) - std::vector<ExecutionTraceEvent*> events; -}; - - class ExecutionState { public: typedef std::vector<StackFrame> stack_ty; @@ -115,9 +88,6 @@ public: unsigned instsSinceCovNew; bool coveredNew; - // for printing execution traces when this state terminates - ExecutionTraceManager exeTraceMgr; - /// Disables forking, set by user code. bool forkDisabled; @@ -166,81 +136,6 @@ public: bool merge(const ExecutionState &b); }; - -// for producing abbreviated execution traces to help visualize -// paths and diagnose bugs - -class ExecutionTraceEvent { -public: - // the location of the instruction: - std::string file; - unsigned line; - std::string funcName; - unsigned stackDepth; - - unsigned consecutiveCount; // init to 1, increase for CONSECUTIVE - // repetitions of the SAME event - - ExecutionTraceEvent() - : file("global"), line(0), funcName("global_def"), - consecutiveCount(1) {} - - ExecutionTraceEvent(ExecutionState& state, KInstruction* ki); - - virtual ~ExecutionTraceEvent() {} - - void print(std::ostream &os) const; - - // return true if it shouldn't be added to ExecutionTraceManager - // - virtual bool ignoreMe() const; - -private: - virtual void printDetails(std::ostream &os) const = 0; -}; - - -class FunctionCallTraceEvent : public ExecutionTraceEvent { -public: - std::string calleeFuncName; - - FunctionCallTraceEvent(ExecutionState& state, KInstruction* ki, - const std::string& _calleeFuncName) - : ExecutionTraceEvent(state, ki), calleeFuncName(_calleeFuncName) {} - -private: - virtual void printDetails(std::ostream &os) const { - os << "CALL " << calleeFuncName; - } - -}; - -class FunctionReturnTraceEvent : public ExecutionTraceEvent { -public: - FunctionReturnTraceEvent(ExecutionState& state, KInstruction* ki) - : ExecutionTraceEvent(state, ki) {} - -private: - virtual void printDetails(std::ostream &os) const { - os << "RETURN"; - } -}; - -class BranchTraceEvent : public ExecutionTraceEvent { -public: - bool trueTaken; // which side taken? - bool canForkGoBothWays; - - BranchTraceEvent(ExecutionState& state, KInstruction* ki, - bool _trueTaken, bool _isTwoWay) - : ExecutionTraceEvent(state, ki), - trueTaken(_trueTaken), - canForkGoBothWays(_isTwoWay) {} - -private: - virtual void printDetails(std::ostream &os) const; -}; - } #endif |