diff options
Diffstat (limited to 'include/klee/util')
-rw-r--r-- | include/klee/util/Assignment.h | 6 | ||||
-rw-r--r-- | include/klee/util/Ref.h | 61 |
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(); } |