diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2021-06-07 16:18:16 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2024-02-29 19:57:08 +0000 |
commit | 8750da62ccb9772a121126d5fffd393690c95758 (patch) | |
tree | 6aa38122cd4c9808d7446ff4e3f8928b01915e23 | |
parent | a4d9762a31402c5e5298ef22870a7e25124a7af2 (diff) | |
download | klee-8750da62ccb9772a121126d5fffd393690c95758.tar.gz |
Use correctly constrained constants if the memory object is fully symbolic
Before, only partially symbolic variables have been concretized. Now, every object that is not fully concrete is concretized correctly this includes fully symbolic objects.
-rw-r--r-- | lib/Core/Memory.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 1e3c8922..0c9394bd 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -199,7 +199,7 @@ const UpdateList &ObjectState::getUpdates() const { void ObjectState::flushToConcreteStore(TimingSolver *solver, const ExecutionState &state) const { for (unsigned i = 0; i < size; i++) { - if (isByteKnownSymbolic(i)) { + if (!isByteConcrete(i)) { ref<ConstantExpr> ce; bool success = solver->getValue(state.constraints, read8(i), ce, state.queryMetaData); |