diff options
Diffstat (limited to 'lib/Core/Memory.h')
-rw-r--r-- | lib/Core/Memory.h | 16 |
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; |