about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2018-05-05 00:02:56 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-05-05 10:35:28 +0100
commit4211cea27f1903f68c2b32267eb34cb95c24b9f3 (patch)
tree8a31d1391bfca40d422112866469c2ac36b3ec11 /lib
parent871fef8da228270f2d57fc76e4d93bb082f4d046 (diff)
downloadklee-4211cea27f1903f68c2b32267eb34cb95c24b9f3.tar.gz
Factor out method to update state memory with process state
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/AddressSpace.cpp25
-rw-r--r--lib/Core/AddressSpace.h9
2 files changed, 25 insertions, 9 deletions
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