about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/Expr.h2
-rw-r--r--include/klee/Solver.h2
-rw-r--r--include/klee/util/ExprRangeEvaluator.h2
3 files changed, 4 insertions, 2 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 2945b697..8f7117bf 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -308,6 +308,8 @@ public:
   unsigned getNumKids() const { return 0; }
   ref<Expr> getKid(unsigned i) const { return 0; }
 
+  uint64_t getConstantValue() const { return asUInt64; }
+
   int compareContents(const Expr &b) const { 
     const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
     if (width != cb.width) return width < cb.width ? -1 : 1;
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 1ed8c175..b8324a9f 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -116,7 +116,7 @@ namespace klee {
     /// satisying assignment.
     ///
     /// \return True on success.
-    bool getValue(const Query&, ref<Expr> &result);
+    bool getValue(const Query&, ref<ConstantExpr> &result);
 
     /// getInitialValues - Compute the initial values for a list of objects.
     ///
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index c5637341..2dafd6ff 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -91,7 +91,7 @@ template<class T>
 T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
   switch (e->getKind()) {
   case Expr::Constant:
-    return T(e->getConstantValue());
+    return T(cast<ConstantExpr>(e)->getConstantValue());
 
   case Expr::NotOptimized: 
     break;