diff options
| -rw-r--r-- | include/klee/ExecutionState.h | 5 | ||||
| -rw-r--r-- | lib/Core/ExecutionState.cpp | 21 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 25 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 2 |
4 files changed, 0 insertions, 53 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 1d2df49a..54915843 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -163,11 +163,6 @@ public: constraints.addConstraint(e); } - // Used for checkpoint/rollback of fake objects created during tainting. - ObjectState *cloneObject(ObjectState *os, MemoryObject *mo); - - // - bool merge(const ExecutionState &b); }; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index d07b6490..9eb560b8 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -303,29 +303,8 @@ bool ExecutionState::merge(const ExecutionState &b) { return true; } -/**/ - -/* - Used for tainting: create a clone of os that we can revirt to with - the behavior that all constraints are preserved, but writes are - discarded. When we revirt it will be at the same address. - */ -ObjectState *ExecutionState::cloneObject(ObjectState *os, - MemoryObject *mo) { - MemoryMap::iterator it = shadowObjects.find(mo); - if (it != shadowObjects.end()) - assert(0 && "Cannot exist already!"); - - llvm::cerr << "DRE: Inserting a cloned object: " << mo << "\n"; - shadowObjects = shadowObjects.replace(std::make_pair(mo, os)); - os = new ObjectState(*os); - addressSpace.bindObject(mo, os); - return os; -} - /***/ - ExecutionTraceEvent::ExecutionTraceEvent(ExecutionState& state, KInstruction* ki) : consecutiveCount(1) diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 11705722..3070da41 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -81,7 +81,6 @@ HandlerInfo handlerInfo[] = { add("klee_set_forking", handleSetForking, false), add("klee_warning", handleWarning, false), add("klee_warning_once", handleWarningOnce, false), - add("klee_under_constrained", handleUnderConstrained, false), add("klee_alias_function", handleAliasFunction, false), add("malloc", handleMalloc, true), add("realloc", handleRealloc, true), @@ -409,30 +408,6 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, llvm::cerr << msg_str << ":" << arguments[1] << "\n"; } - -void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - // XXX should type check args - assert(arguments.size()==1 && - "invalid number of arguments to klee_under_constrained()."); - assert(isa<ConstantExpr>(arguments[0]) && - "symbolic argument given to klee_under_constrained!"); - - unsigned v = cast<ConstantExpr>(arguments[0])->getConstantValue(); - llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n"; - if(v) { - assert(state.underConstrained == false && - "Bogus call to klee_under_constrained()."); - state.underConstrained = v; - llvm::cerr << "turning on under!\n"; - } else { - assert(state.underConstrained != 0 && "Bogus call to klee_taint_end()"); - state.underConstrained = 0; - llvm::cerr << "turning off under!\n"; - } -} - void SpecialFunctionHandler::handleSetForking(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 3d5c459b..a6cc7aa8 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -669,10 +669,8 @@ static const char *modelledExternals[] = { "klee_print_expr", "klee_print_range", "klee_report_error", - "klee_revirt_objects", "klee_set_forking", "klee_silent_exit", - "klee_under_constrained", "klee_warning", "klee_warning_once", "klee_alias_function", |