aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
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 /lib
parenteb4f9b5b6e674530fa1a011889380d0cce76caef (diff)
downloadklee-61332cd6174b88148c4f891845ab181f0ee054ca.tar.gz
Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilder
Diffstat (limited to 'lib')
-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) {