From 76a2adef91dc987083e8e30f40c4143742e4e726 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 27 Feb 2024 16:20:11 +0000 Subject: Add support to fully concretise objects if modified externally Propagate ExternalCallPolicy to allow user-based selection. --- lib/Core/AddressSpace.h | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'lib/Core/AddressSpace.h') 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 -- cgit 1.4.1