diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Memory.cpp | 4 | ||||
-rw-r--r-- | lib/Core/SeedInfo.cpp | 4 |
2 files changed, 3 insertions, 5 deletions
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 8f144456..ba1b8e1f 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -102,7 +102,7 @@ ObjectState::ObjectState(const MemoryObject *mo, unsigned _size) flushMask(0), knownSymbolics(0), size(_size), - updates(mo->array, false, 0), + updates(mo->array, 0), readOnly(false) { } @@ -149,7 +149,6 @@ void ObjectState::makeConcrete() { void ObjectState::makeSymbolic() { assert(!updates.head && "XXX makeSymbolic of objects with symbolic values is unsupported"); - updates.isRooted = true; // XXX simplify this, can just delete various arrays I guess for (unsigned i=0; i<size; i++) { @@ -792,7 +791,6 @@ void ObjectState::print() { llvm::cerr << "-- ObjectState --\n"; llvm::cerr << "\tMemoryObject ID: " << object->id << "\n"; llvm::cerr << "\tRoot Object: " << updates.root << "\n"; - llvm::cerr << "\tIs Rooted? " << updates.isRooted << "\n"; llvm::cerr << "\tSize: " << size << "\n"; llvm::cerr << "\tBytes:\n"; diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 6fcfe596..dc3ff931 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -87,7 +87,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, it = directReads.begin(), ie = directReads.end(); it != ie; ++it) { const Array *array = it->first; unsigned i = it->second; - ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0), + ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); // If not in bindings then this can't be a violation? @@ -124,7 +124,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, ie = assignment.bindings.end(); it != ie; ++it) { const Array *array = it->first; for (unsigned i=0; i<array->size; ++i) { - ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0), + ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)); bool res; |