Create new ObjectState constructor for explicitly creating symbolic objects.

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

1 files changed, 15 insertions, 10 deletions

diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 565572be..85f83ee1 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -160,9 +160,15 @@ public:
   bool readOnly;
 
 public:
-  // initial contents are undefined but concrete, it is the creators
-  // responsibility to initialize the object contents appropriate
-  ObjectState(const MemoryObject *mo, unsigned size);
+  /// Create a new object state for the given memory object with concrete
+  /// contents. The initial contents are undefined, it is the callers
+  /// responsibility to initialize the object contents appropriately.
+  ObjectState(const MemoryObject *mo);
+
+  /// Create a new object state for the given memory object with symbolic
+  /// contents.
+  ObjectState(const MemoryObject *mo, const Array *array);
+
   ObjectState(const ObjectState &os);
   ~ObjectState();
 
@@ -170,11 +176,6 @@ public:
 
   void setReadOnly(bool ro) { readOnly = ro; }
 
-  // make all bytes are concrete with undefined values
-  void makeConcrete();
-
-  void makeSymbolic();
-
   // make contents all concrete and zero
   void initializeToZero();
   // make contents all concrete and random
@@ -198,6 +199,10 @@ public:
   void write64(unsigned offset, uint64_t value);
 
 private:
+  void makeConcrete();
+
+  void makeSymbolic();
+
   ref<Expr> read1(ref<Expr> offset) const;
   ref<Expr> read8(ref<Expr> offset) const;
   ref<Expr> read16(ref<Expr> offset) const;
@@ -215,8 +220,8 @@ private:
   void write64(unsigned offset, ref<Expr> value);
   void write64(ref<Expr> offset, ref<Expr> value);
 
-  
-  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, unsigned *size_r) const;
+  void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, 
+                            unsigned *size_r) const;
   void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
   void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);