aboutsummaryrefslogtreecommitdiffhomepage
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;