Change ExecutionState::symbolics to include both the MemoryObject and the

symbolic Array.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73161 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 4 insertions, 3 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 09ce2a4b..1d2df49a 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 namespace klee {
+  class Array;
   class CallPathNode;
   class Cell;
   class KFunction;
@@ -126,7 +127,7 @@ public:
   /// ordered list of symbolics: used to generate test cases. 
   //
   // FIXME: Move to a shared list structure (not critical).
-  std::vector<const MemoryObject*> symbolics;
+  std::vector< std::pair<const MemoryObject*, const Array*> > symbolics;
 
   // Used by the checkpoint/rollback methods for fake objects.
   // FIXME: not freeing things on branch deletion.
@@ -155,8 +156,8 @@ public:
   void pushFrame(KInstIterator caller, KFunction *kf);
   void popFrame();
 
-  void addSymbolic(const MemoryObject *mo) { 
-    symbolics.push_back(mo);
+  void addSymbolic(const MemoryObject *mo, const Array *array) { 
+    symbolics.push_back(std::make_pair(mo, array));
   }
   void addConstraint(ref<Expr> e) { 
     constraints.addConstraint(e);