about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2021-06-07 16:18:16 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2024-02-29 19:57:08 +0000
commit8750da62ccb9772a121126d5fffd393690c95758 (patch)
tree6aa38122cd4c9808d7446ff4e3f8928b01915e23
parenta4d9762a31402c5e5298ef22870a7e25124a7af2 (diff)
downloadklee-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.cpp2
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);