Asserting that update lists have non-NULL roots within ReadExpr objects (update

lists can have NULL roots, e.g. in MemoryObject instances with concrete
contents, where root is allocated lazily only when the updates are required).
Also checking whether array updates are typed correctly in UpdateList::extend()
rather than in the constructor of UpdateNode (only for update lists with
non-NULL roots).

2 files changed, 8 insertions, 2 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 240c6220..a302591a 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -675,7 +675,7 @@ public:
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
   
-  Width getWidth() const { return updates.root ? updates.root->getRange() : Expr::Int8; }
+  Width getWidth() const { assert(updates.root); return updates.root->getRange(); }
   Kind getKind() const { return Read; }
   
   unsigned getNumKids() const { return numKids; }
@@ -691,7 +691,7 @@ public:
 
 private:
   ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) : 
-    updates(_updates), index(_index) {}
+    updates(_updates), index(_index) { assert(updates.root); }
 
 public:
   static bool classof(const Expr *E) {
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 107cf9d4..bf7049ba 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -88,6 +88,12 @@ UpdateList &UpdateList::operator=(const UpdateList &b) {
 }
 
 void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
+  
+  if (root) {
+    assert(root->getDomain() == index->getWidth());
+    assert(root->getRange() == value->getWidth());
+  }
+
   if (head) --head->refCount;
   head = new UpdateNode(head, index, value);
   ++head->refCount;