about summary refs log tree commit diff homepage
path: root/lib/Core/Memory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Memory.cpp')
-rw-r--r--lib/Core/Memory.cpp16
1 files changed, 16 insertions, 0 deletions
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index cd13eada..5c855fb8 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -229,6 +229,22 @@ const UpdateList &ObjectState::getUpdates() const {
   return updates;
 }
 
+void ObjectState::flushToConcreteStore(TimingSolver *solver,
+                                       const ExecutionState &state) const {
+  for (unsigned i = 0; i < size; i++) {
+    if (isByteKnownSymbolic(i)) {
+      ref<ConstantExpr> ce;
+      bool success = solver->getValue(state, read8(i), ce);
+      if (!success)
+        klee_warning("Solver timed out when getting a value for external call, "
+                     "byte %p+%u will have random value",
+                     (void *)object->address, i);
+      else
+        ce->toMemory(concreteStore + i);
+    }
+  }
+}
+
 void ObjectState::makeConcrete() {
   delete concreteMask;
   delete flushMask;