Associate a domain and range with each array

1 files changed, 10 insertions, 6 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index f893c6cc..ee3c3253 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -587,7 +587,9 @@ public:
   /// a symbolic array. If non-empty, this size of this array is equivalent to
   /// the array size.
   const std::vector< ref<ConstantExpr> > constantValues;
-  
+
+  Expr::Width domain, range;
+
 public:
   /// Array - Construct a new array object.
   ///
@@ -598,9 +600,11 @@ public:
   /// distinguished once printed.
   Array(const std::string &_name, uint64_t _size, 
         const ref<ConstantExpr> *constantValuesBegin = 0,
-        const ref<ConstantExpr> *constantValuesEnd = 0)
+        const ref<ConstantExpr> *constantValuesEnd = 0,
+        Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8)
     : name(_name), size(_size), 
-      constantValues(constantValuesBegin, constantValuesEnd) {      
+      constantValues(constantValuesBegin, constantValuesEnd),
+      domain(_domain), range(_range) {
     assert((isSymbolicArray() || constantValues.size() == size) &&
            "Invalid size for constant array!");
     computeHash();
@@ -616,8 +620,8 @@ public:
   bool isSymbolicArray() const { return constantValues.empty(); }
   bool isConstantArray() const { return !isSymbolicArray(); }
 
-  Expr::Width getDomain() const { return Expr::Int32; }
-  Expr::Width getRange() const { return Expr::Int8; }
+  Expr::Width getDomain() const { return domain; }
+  Expr::Width getRange() const { return range; }
   
   unsigned computeHash();
   unsigned hash() const { return hashValue; }
@@ -671,7 +675,7 @@ public:
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
   
-  Width getWidth() const { return Expr::Int8; }
+  Width getWidth() const { return updates.root->getRange(); }
   Kind getKind() const { return Read; }
   
   unsigned getNumKids() const { return numKids; }