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 /lib/Core/Executor.cpp | |
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 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 87e6bb29..26c082af 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -75,9 +75,6 @@ using namespace llvm; using namespace klee; -// omg really hard to share cl opts across files ... -bool WriteTraces = false; - namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", @@ -246,13 +243,6 @@ namespace { cl::desc("Inhibit forking at memory cap (vs. random terminate)"), cl::init(true)); - // use 'external storage' because also needed by tools/klee/main.cpp - cl::opt<bool, true> - WriteTracesProxy("write-traces", - cl::desc("Write .trace file for each terminated state"), - cl::location(WriteTraces), - cl::init(false)); - cl::opt<bool> UseForkedSTP("use-forked-stp", cl::desc("Run STP in forked process")); @@ -1096,10 +1086,6 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, std::vector< ref<Expr> > &arguments) { - if (WriteTraces) - state.exeTraceMgr.addEvent(new FunctionCallTraceEvent(state, ki, - f->getName())); - Instruction *i = ki->inst; if (f && f->isDeclaration()) { switch(f->getIntrinsicID()) { @@ -1320,10 +1306,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *caller = kcaller ? kcaller->inst : 0; bool isVoidReturn = (ri->getNumOperands() == 0); ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool); - - if (WriteTraces) { - state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki)); - } if (!isVoidReturn) { result = eval(ki, 0, state).value; @@ -1409,20 +1391,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<Expr> cond = eval(ki, 0, state).value; Executor::StatePair branches = fork(state, cond, false); - if (WriteTraces) { - bool isTwoWay = (branches.first && branches.second); - - if (branches.first) { - branches.first->exeTraceMgr.addEvent( - new BranchTraceEvent(state, ki, true, isTwoWay)); - } - - if (branches.second) { - branches.second->exeTraceMgr.addEvent( - new BranchTraceEvent(state, ki, false, isTwoWay)); - } - } - // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch // instruction (it reuses its statistic id). Should be cleaned |