diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 04:23:54 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 04:23:54 +0000 |
commit | 380ca8863db645f0c00843af2fef575b655783ff (patch) | |
tree | 843cb4a2e71da3d150d8360f6c293204923e1093 /lib/Core | |
parent | 92e1bf7b665a7f5ec682becb78e014e62d10beec (diff) | |
download | klee-380ca8863db645f0c00843af2fef575b655783ff.tar.gz |
Add several ConstantExpr utility functions and move clients over.
- Reducing uses of getConstantValue() so we can move to arbitrary precision constants. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73324 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 20 | ||||
-rw-r--r-- | lib/Core/TimingSolver.cpp | 4 |
2 files changed, 11 insertions, 13 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2aae57c9..f12aec08 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -630,7 +630,7 @@ void Executor::branch(ExecutionState &state, res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (res->getConstantValue()) + if (res->isTrue()) break; } @@ -766,15 +766,13 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { solver->getValue(current, siit->assignment.evaluate(condition), res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (ConstantExpr *CE = dyn_cast<ConstantExpr>(res)) { - if (CE->getConstantValue()) { - trueSeed = true; - } else { - falseSeed = true; - } - if (trueSeed && falseSeed) - break; + if (res->isTrue()) { + trueSeed = true; + } else { + falseSeed = true; } + if (trueSeed && falseSeed) + break; } if (!(trueSeed && falseSeed)) { assert(trueSeed || falseSeed); @@ -832,7 +830,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { solver->getValue(current, siit->assignment.evaluate(condition), res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (res->getConstantValue()) { + if (res->isTrue()) { trueSeeds.push_back(*siit); } else { falseSeeds.push_back(*siit); @@ -889,7 +887,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) { - assert(CE->getConstantValue() && "attempt to add invalid constraint"); + assert(CE->isTrue() && "attempt to add invalid constraint"); return; } diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 339c33b2..0154ddcf 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -26,7 +26,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr, Solver::Validity &result) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) { - result = CE->getConstantValue() ? Solver::True : Solver::False; + result = CE->isTrue() ? Solver::True : Solver::False; return true; } @@ -50,7 +50,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, bool &result) { // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) { - result = CE->getConstantValue() ? true : false; + result = CE->isTrue() ? true : false; return true; } |