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

---
 lib/Expr/Updates.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/Expr/Updates.cpp')

diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 14fd8308..107cf9d4 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -22,8 +22,12 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
     next(_next),
     index(_index),
     value(_value) {
+  // FIXME: What we need to check here instead is that _value is of the same width 
+  // as the range of the array that the update node is part of.
+  /*
   assert(_value->getWidth() == Expr::Int8 && 
          "Update value should be 8-bit wide.");
+  */
   computeHash();
   if (next) {
     ++next->refCount;
-- 
cgit 1.4.1


From 2795655e567c3cdbfe3d4815edd83b4f4cdbb542 Mon Sep 17 00:00:00 2001
From: Hristina Palikareva <h.palikareva@imperial.ac.uk>
Date: Wed, 23 Apr 2014 20:20:33 +0100
Subject: 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).

---
 include/klee/Expr.h  | 4 ++--
 lib/Expr/Updates.cpp | 6 ++++++
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'lib/Expr/Updates.cpp')

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;
-- 
cgit 1.4.1