aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver/STPBuilder.cpp
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-14 04:23:54 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-14 04:23:54 +0000
commit380ca8863db645f0c00843af2fef575b655783ff (patch)
tree843cb4a2e71da3d150d8360f6c293204923e1093 /lib/Solver/STPBuilder.cpp
parent92e1bf7b665a7f5ec682becb78e014e62d10beec (diff)
downloadklee-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/Solver/STPBuilder.cpp')
-rw-r--r--lib/Solver/STPBuilder.cpp11
1 files changed, 5 insertions, 6 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ab65f254..8680d0a8 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -608,11 +608,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
assert(*width_out!=1 && "uncanonicalized sdiv");
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
- uint64_t divisor = CE->getConstantValue();
-
if (optimizeDivides) {
if (*width_out == 32) //only works for 32-bit division
- return constructSDivByConstant( left, *width_out, divisor);
+ return constructSDivByConstant( left, *width_out,
+ CE->getConstantValue());
}
}
@@ -776,9 +775,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
ExprHandle left = construct(ee->left, width_out);
ExprHandle right = construct(ee->right, width_out);
if (*width_out==1) {
- if (isa<ConstantExpr>(ee->left)) {
- assert(!cast<ConstantExpr>(ee->left)->getConstantValue() &&
- "uncanonicalized eq");
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+ if (CE->isTrue())
+ return right;
return vc_notExpr(vc, right);
} else {
return vc_iffExpr(vc, left, right);