From 7561acc8b346028bc6eb586ea76b5b2a9400140c Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Wed, 10 Jun 2009 06:18:37 +0000 Subject: 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 --- include/klee/ExecutionState.h | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'include') 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 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 symbolics; + std::vector< std::pair > 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 e) { constraints.addConstraint(e); -- cgit 1.4.1