Add support to fully concretise objects if modified externally

Propagate ExternalCallPolicy to allow user-based selection.

1 files changed, 8 insertions, 4 deletions

diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 37ae76f9..fa4fb940 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -138,18 +138,22 @@ namespace klee {
     /// potentially copied) if the memory values are different from
     /// the current concrete values.
     ///
-    /// \retval true The copy succeeded. 
-    /// \retval false The copy failed because a read-only object was modified.
-    bool copyInConcretes();
+    /// \param concretize fully concretize the object representation if changed
+    /// externally
+    /// \return true if copy succeeded, otherwise false (e.g. try to modify
+    /// read-only object)
+    bool copyInConcretes(bool concretize);
 
     /// 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
+    /// @param concretize fully concretize the object representation if changed
+    /// externally
     /// @return
     bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
-                        uint64_t src_address);
+                        uint64_t src_address, bool concretize);
   };
 } // End klee namespace