about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-12-04 14:20:52 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2015-12-04 14:20:52 +0000
commit61332cd6174b88148c4f891845ab181f0ee054ca (patch)
treee8e4a3249656ed48e209b080a67aa3a969fb5b55
parenteb4f9b5b6e674530fa1a011889380d0cce76caef (diff)
downloadklee-61332cd6174b88148c4f891845ab181f0ee054ca.tar.gz
Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilder
-rw-r--r--lib/Solver/STPBuilder.cpp20
-rw-r--r--lib/Solver/STPBuilder.h2
2 files changed, 3 insertions, 19 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ddeb3c37..4bd0145f 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -72,13 +72,9 @@ STPArrayExprHash::~STPArrayExprHash() {
 
 /***/
 
-STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides) 
-  : vc(_vc), optimizeDivides(_optimizeDivides)
-{
-  tempVars[0] = buildVar("__tmpInt8", 8);
-  tempVars[1] = buildVar("__tmpInt16", 16);
-  tempVars[2] = buildVar("__tmpInt32", 32);
-  tempVars[3] = buildVar("__tmpInt64", 64);
+STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides)
+  : vc(_vc), optimizeDivides(_optimizeDivides) {
+
 }
 
 STPBuilder::~STPBuilder() {
@@ -111,16 +107,6 @@ STPBuilder::~STPBuilder() {
   return res;
 }
 
-ExprHandle STPBuilder::getTempVar(Expr::Width w) {
-  switch (w) {
-  default: assert(0 && "invalid type");
-  case Expr::Int8: return tempVars[0];
-  case Expr::Int16: return tempVars[1];
-  case Expr::Int32: return tempVars[2];
-  case Expr::Int64: return tempVars[3];
-  }
-}
-
 ExprHandle STPBuilder::getTrue() {
   return vc_trueExpr(vc);
 }
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index ef1cd8b3..e196a064 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -68,7 +68,6 @@ namespace klee {
 
 class STPBuilder {
   ::VC vc;
-  ExprHandle tempVars[4];
   ExprHashMap< std::pair<ExprHandle, unsigned> > constructed;
 
   /// optimizeDivides - Rewrite division and reminders by constants
@@ -120,7 +119,6 @@ public:
 
   ExprHandle getTrue();
   ExprHandle getFalse();
-  ExprHandle getTempVar(Expr::Width w);
   ExprHandle getInitialRead(const Array *os, unsigned index);
 
   ExprHandle construct(ref<Expr> e) {