From 4211cea27f1903f68c2b32267eb34cb95c24b9f3 Mon Sep 17 00:00:00 2001
From: Martin Nowack <martin.nowack@gmail.com>
Date: Sat, 5 May 2018 00:02:56 +0100
Subject: Factor out method to update state memory with process state

---
 lib/Core/AddressSpace.cpp | 25 ++++++++++++++++---------
 lib/Core/AddressSpace.h   |  9 +++++++++
 2 files changed, 25 insertions(+), 9 deletions(-)

(limited to 'lib')

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 811e52c3..2169ed06 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -313,22 +313,29 @@ bool AddressSpace::copyInConcretes() {
 
     if (!mo->isUserSpecified) {
       const ObjectState *os = it->second;
-      uint8_t *address = (uint8_t*) (unsigned long) mo->address;
 
-      if (memcmp(address, os->concreteStore, mo->size)!=0) {
-        if (os->readOnly) {
-          return false;
-        } else {
-          ObjectState *wos = getWriteable(mo, os);
-          memcpy(wos->concreteStore, address, mo->size);
-        }
-      }
+      if (!copyInConcrete(mo, os, mo->address))
+        return false;
     }
   }
 
   return true;
 }
 
+bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
+                                  uint64_t src_address) {
+  uint8_t *address = (uint8_t *)(unsigned long)src_address;
+  if (memcmp(address, os->concreteStore, mo->size) != 0) {
+    if (os->readOnly) {
+      return false;
+    } else {
+      ObjectState *wos = getWriteable(mo, os);
+      memcpy(wos->concreteStore, address, mo->size);
+    }
+  }
+  return true;
+}
+
 /***/
 
 bool MemoryObjectLT::operator()(const MemoryObject *a, const MemoryObject *b) const {
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 079453b3..10549e7a 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -125,6 +125,15 @@ namespace klee {
     /// \retval true The copy succeeded. 
     /// \retval false The copy failed because a read-only object was modified.
     bool copyInConcretes();
+
+    /// Updates the memory object with the raw memory from the address
+    ///
+    /// @param mo The MemoryObject to update
+    /// @param os The associated memory state containing the actual data
+    /// @param src_address the address to copy from
+    /// @return
+    bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
+                        uint64_t src_address);
   };
 } // End klee namespace
 
-- 
cgit 1.4.1