about summary refs log tree commit diff homepage
path: root/lib/Core/Memory.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Memory.h')
-rw-r--r--lib/Core/Memory.h16
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;