Refactor `ObjectState::flushToConcreteStore` to use `toConstant`

Use existing `Executor::toConstant()` function to transform a symbolic
byte of an `ObjectState` to its concrete representation.

This will also add constraints if required.

1 files changed, 10 insertions, 6 deletions

diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 9a936746..3b365c20 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -29,6 +29,7 @@ namespace klee {
 class ArrayCache;
 class BitArray;
 class ExecutionState;
+class Executor;
 class MemoryManager;
 class Solver;
 
@@ -233,12 +234,15 @@ public:
   void write64(unsigned offset, uint64_t value);
   void print() const;
 
-  /*
-    Looks at all the symbolic bytes of this object, gets a value for them
-    from the solver and puts them in the concreteStore.
-  */
-  void flushToConcreteStore(TimingSolver *solver,
-                            const ExecutionState &state) const;
+  /// Generate concrete values for each symbolic byte of the object and put them
+  /// in the concrete store.
+  ///
+  /// \param executor
+  /// \param state
+  /// \param concretize if true, constraints for concretised bytes are added if
+  /// necessary
+  void flushToConcreteStore(Executor &executor, ExecutionState &state,
+                            bool concretize);
 
 private:
   const UpdateList &getUpdates() const;