about summary refs log tree commit diff homepage
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);