From aa8cc67c0d8c16388ebe670757327a81f774d0ee Mon Sep 17 00:00:00 2001
From: Hristina Palikareva <h.palikareva@imperial.ac.uk>
Date: Wed, 16 Apr 2014 17:56:13 +0100
Subject: Removing a few more hard-coded values for domains and ranges of Array
 objects

---
 include/klee/Expr.h                    | 6 +++---
 include/klee/util/Assignment.h         | 7 ++++---
 include/klee/util/ExprRangeEvaluator.h | 2 +-
 3 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'include')

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index ee3c3253..240c6220 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -675,15 +675,15 @@ public:
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
   
-  Width getWidth() const { return updates.root->getRange(); }
+  Width getWidth() const { return updates.root ? updates.root->getRange() : Expr::Int8; }
   Kind getKind() const { return Read; }
   
   unsigned getNumKids() const { return numKids; }
-  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }  
+  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
   
   int compareContents(const Expr &b) const;
 
-  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
     return create(updates, kids[0]);
   }
 
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 838d03bd..63df4b65 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -67,15 +67,16 @@ namespace klee {
 
   inline ref<Expr> Assignment::evaluate(const Array *array, 
                                         unsigned index) const {
+    assert(array);
     bindings_ty::const_iterator it = bindings.find(array);
     if (it!=bindings.end() && index<it->second.size()) {
-      return ConstantExpr::alloc(it->second[index], Expr::Int8);
+      return ConstantExpr::alloc(it->second[index], array->getRange());
     } else {
       if (allowFreeValues) {
         return ReadExpr::create(UpdateList(array, 0), 
-                                ConstantExpr::alloc(index, Expr::Int32));
+                                ConstantExpr::alloc(index, array->getDomain()));
       } else {
-        return ConstantExpr::alloc(0, Expr::Int8);
+        return ConstantExpr::alloc(0, array->getRange());
       }
     }
   }
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index 34b85520..fea30b5b 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -102,7 +102,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     const ReadExpr *re = cast<ReadExpr>(e);
     T index = evaluate(re->index);
 
-    assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read");
+    assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read");
 
     return evalRead(re->updates, index);
   }
-- 
cgit 1.4.1