Switch to using constant arrays for non-symbolic objects.

 - Currently uses a dumb implementation which keeps the old flushing
   architecture, but converts to a constant array when the first ReadExpr is
   created.

 - Temporary --use-constant-arrays switch can be used to disable for testing.


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

1 files changed, 5 insertions, 3 deletions

diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 85f83ee1..d9849d2e 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -151,12 +151,12 @@ private:
 
   ref<Expr> *knownSymbolics;
 
-public:
-  unsigned size;
-
   // mutable because we may need flush during read of const
   mutable UpdateList updates;
 
+public:
+  unsigned size;
+
   bool readOnly;
 
 public:
@@ -199,6 +199,8 @@ public:
   void write64(unsigned offset, uint64_t value);
 
 private:
+  const UpdateList &getUpdates() const;
+
   void makeConcrete();
 
   void makeSymbolic();