diff options
| -rw-r--r-- | include/klee/Expr.h | 9 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 4 | ||||
| -rw-r--r-- | lib/Core/Memory.h | 4 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 4 | ||||
| -rw-r--r-- | unittests/Expr/ExprTest.cpp | 8 | ||||
| -rw-r--r-- | unittests/Solver/SolverTest.cpp | 2 |
6 files changed, 15 insertions, 16 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index f13ab6d5..73734da3 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -29,7 +29,6 @@ namespace klee { class Array; class ConstantExpr; class ObjectState; -class MemoryObject; template<class T> class ref; @@ -474,8 +473,6 @@ private: class Array { public: const std::string name; - // FIXME: This does not belong here. - const MemoryObject *object; // FIXME: Not 64-bit clean. unsigned size; @@ -485,13 +482,13 @@ public: public: /// Array - Construct a new array object. /// - /// \param _name - The name for this arrays. Names should generally be unique + /// \param _name - The name for this array. Names should generally be unique /// across an application, but this is not necessary for correctness, except /// when printing expressions. When expressions are printed the output will /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. - Array(const std::string &_name, const MemoryObject *_object, uint64_t _size) - : name(_name), object(_object), size(_size), stpInitialArray(0) {} + Array(const std::string &_name, uint64_t _size) + : name(_name), size(_size), stpInitialArray(0) {} ~Array() { // FIXME: This relies on caller to delete the STP array. assert(!stpInitialArray && "Array must be deleted by caller!"); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ab2e106a..e47dcfc0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3199,6 +3199,8 @@ void Executor::getCoveredLines(const ExecutionState &state, void Executor::doImpliedValueConcretization(ExecutionState &state, ref<Expr> e, ref<ConstantExpr> value) { + abort(); // FIXME: Broken until we sort out how to do the write back. + if (DebugCheckForImpliedValues) ImpliedValue::checkForImpliedValues(solver->solver, e, value); @@ -3211,7 +3213,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) { // FIXME: This is the sole remaining usage of the Array object // variable. Kill me. - const MemoryObject *mo = re->updates.root->object; + const MemoryObject *mo = 0; //re->updates.root->object; const ObjectState *os = state.addressSpace.findObject(mo); if (!os) { diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 141060d0..b6ea81d7 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -71,7 +71,7 @@ public: MemoryObject(uint64_t _address) : id(counter++), address(_address), - array(new Array("arr" + llvm::utostr(id), this, id)), + array(new Array("arr" + llvm::utostr(id), id)), size(0), isFixed(true), allocSite(0) { @@ -82,7 +82,7 @@ public: const llvm::Value *_allocSite) : id(counter++), address(_address), - array(new Array("arr" + llvm::utostr(id), this, _size)), + array(new Array("arr" + llvm::utostr(id), _size)), size(_size), name("unnamed"), isLocal(_isLocal), diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 856541ee..8e5349c5 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -519,7 +519,7 @@ DeclResult ParserImpl::ParseArrayDecl() { // FIXME: Array should take domain and range. const Identifier *Label = GetOrCreateIdentifier(Name); - Array *Root = new Array(Label->Name, 0, Size.get()); + Array *Root = new Array(Label->Name, Size.get()); ArrayDecl *AD = new ArrayDecl(Label, Size.get(), DomainType.get(), RangeType.get(), Root); @@ -1298,7 +1298,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() { VersionResult Res = ParseVersion(); // Define update list to avoid use-of-undef errors. if (!Res.isValid()) { - Res = VersionResult(true, UpdateList(new Array("", 0, 0), NULL)); + Res = VersionResult(true, UpdateList(new Array("", 0), NULL)); } if (Label) diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index b5f02b83..4b56f472 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -28,9 +28,9 @@ TEST(ExprTest, BasicConstruction) { } TEST(ExprTest, ConcatExtract) { - Array *array = new Array("arr0", 0, 256); + Array *array = new Array("arr0", 256); ref<Expr> read8 = Expr::createTempRead(array, 8); - Array *array2 = new Array("arr1", 0, 256); + Array *array2 = new Array("arr1", 256); ref<Expr> read8_2 = Expr::createTempRead(array2, 8); ref<Expr> c100 = getConstant(100, 8); @@ -80,10 +80,10 @@ TEST(ExprTest, ConcatExtract) { } TEST(ExprTest, ExtractConcat) { - Array *array = new Array("arr2", 0, 256); + Array *array = new Array("arr2", 256); ref<Expr> read64 = Expr::createTempRead(array, 64); - Array *array2 = new Array("arr3", 0, 256); + Array *array2 = new Array("arr3", 256); ref<Expr> read8_2 = Expr::createTempRead(array2, 8); ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4); diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 87ec63ef..cda0cf96 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -45,7 +45,7 @@ void testOperation(Solver &solver, unsigned size = Expr::getMinBytesForWidth(operandWidth); static uint64_t id = 0; - Array *array = new Array("arr" + llvm::utostr(++id), 0, size); + Array *array = new Array("arr" + llvm::utostr(++id), size); symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, operandWidth))); } |