about summary refs log tree commit diff homepage
path: root/include/klee/util
diff options
context:
space:
mode:
Diffstat (limited to 'include/klee/util')
-rw-r--r--include/klee/util/Assignment.h6
-rw-r--r--include/klee/util/Ref.h61
2 files changed, 14 insertions, 53 deletions
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 19f89a03..cb001415 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -69,13 +69,13 @@ namespace klee {
                                         unsigned index) const {
     bindings_ty::const_iterator it = bindings.find(array);
     if (it!=bindings.end() && index<it->second.size()) {
-      return ref<Expr>(it->second[index], Expr::Int8);
+      return ConstantExpr::alloc(it->second[index], Expr::Int8);
     } else {
       if (allowFreeValues) {
         return ReadExpr::create(UpdateList(array, true, 0), 
-                                ref<Expr>(index, Expr::Int32));
+                                ConstantExpr::alloc(index, Expr::Int32));
       } else {
-        return ref<Expr>(0, Expr::Int8);
+        return ConstantExpr::alloc(0, Expr::Int8);
       }
     }
   }
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index a70b09cf..f900f137 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -13,48 +13,11 @@
 #include <assert.h>
 
 class Expr;
-class BinaryExpr;
-class CastExpr;
-class CmpExpr;
-
 class ConstantExpr;
-class ReadExpr;
-class UpdateNode;
-class NotOptimizedExpr;
-class ReadExpr;
-class SelectExpr;
-class ConcatExpr;
-class ExtractExpr;
-class ZExtExpr;
-class SExtExpr;
-class AddExpr;
-class SubExpr;
-class MulExpr;
-class UDivExpr;
-class SDivExpr;
-class URemExpr;
-class SRemExpr;
-class AndExpr;
-class OrExpr;
-class XorExpr;
-class ShlExpr;
-class LShrExpr;
-class AShrExpr;
-class EqExpr;
-class NeExpr;
-class UltExpr;
-class UleExpr;
-class UgtExpr;
-class UgeExpr;
-class SltExpr;
-class SleExpr;
-class SgtExpr;
-class SgeExpr;
-class KModule;
-
-  class ExprVisitor;
-  class StackFrame;
-  class ObjectState;
+
+class ExprVisitor;
+class StackFrame;
+class ObjectState;
 
 template<class T>
 class ref {
@@ -91,9 +54,12 @@ private:
   }  
 
   friend class ExprVisitor;
-  friend class Cell;
-  friend class ObjectState;
-  friend class KModule;
+  friend class ConstantExpr;
+
+  // construct from constant
+  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+    contents.val = val;
+  }
 
 public:
   template<class U> friend class ref;
@@ -107,14 +73,9 @@ public:
     contents.ptr = p;
     inc();
   }
-
-  // construct from constant
-  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
-    contents.val = val;
-  }
   
   // normal copy constructor
-  ref (const ref<T> &r)
+  ref(const ref<T> &r)
     : constantWidth(r.constantWidth), contents(r.contents) {
     inc();
   }