diff options
author | Martin Nowack <martin.nowack@gmail.com> | 2018-05-05 00:02:56 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-05 10:35:28 +0100 |
commit | 4211cea27f1903f68c2b32267eb34cb95c24b9f3 (patch) | |
tree | 8a31d1391bfca40d422112866469c2ac36b3ec11 /lib | |
parent | 871fef8da228270f2d57fc76e4d93bb082f4d046 (diff) | |
download | klee-4211cea27f1903f68c2b32267eb34cb95c24b9f3.tar.gz |
Factor out method to update state memory with process state
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/AddressSpace.cpp | 25 | ||||
-rw-r--r-- | lib/Core/AddressSpace.h | 9 |
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 |