From 4211cea27f1903f68c2b32267eb34cb95c24b9f3 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sat, 5 May 2018 00:02:56 +0100 Subject: Factor out method to update state memory with process state --- lib/Core/AddressSpace.h | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'lib/Core/AddressSpace.h') 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