Clean up a number of unused variable warnings when building w/o

asserts.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72924 91177308-0d34-0410-b5e6-96231b3b80d8

11 files changed, 66 insertions, 28 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index bbaa55e4..d58fdc81 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -320,6 +320,7 @@ public:
 
   virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
     assert(0 && "rebuild() on ConstantExpr"); 
+    return (Expr*) this;
   }
 
   virtual unsigned computeHash();
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index fece4af9..ab2e106a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -628,6 +628,7 @@ void Executor::branch(ExecutionState &state,
           solver->getValue(state, siit->assignment.evaluate(conditions[i]), 
                            res);
         assert(success && "FIXME: Unhandled solver failure");
+        (void) success;
         if (res->getConstantValue())
           break;
       }
@@ -683,6 +684,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       ref<ConstantExpr> value; 
       bool success = solver->getValue(current, condition, value);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       addConstraint(current, EqExpr::create(value, condition));
       condition = value;
     }      
@@ -752,6 +754,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       bool success = 
         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;
@@ -817,6 +820,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         bool success = 
           solver->getValue(current, siit->assignment.evaluate(condition), res);
         assert(success && "FIXME: Unhandled solver failure");
+        (void) success;
         if (res->getConstantValue()) {
           trueSeeds.push_back(*siit);
         } else {
@@ -889,6 +893,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
       bool success = 
         solver->mustBeFalse(state, siit->assignment.evaluate(condition), res);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       if (res) {
         siit->patchSeed(state, condition, solver);
         warn = true;
@@ -1026,6 +1031,7 @@ Executor::toConstant(ExecutionState &state,
   ref<ConstantExpr> value;
   bool success = solver->getValue(state, e, value);
   assert(success && "FIXME: Unhandled solver failure");
+  (void) success;
     
   std::ostringstream os;
   os << "silently concretizing (reason: " << reason << ") expression " << e 
@@ -1052,6 +1058,7 @@ void Executor::executeGetValue(ExecutionState &state,
     ref<ConstantExpr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
+    (void) success;
     bindLocal(target, state, value);
   } else {
     std::set< ref<Expr> > values;
@@ -1061,6 +1068,7 @@ void Executor::executeGetValue(ExecutionState &state,
       bool success = 
         solver->getValue(state, siit->assignment.evaluate(e), value);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       values.insert(value);
     }
     
@@ -1409,6 +1417,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         bool result;
         bool success = solver->mayBeTrue(state, match, result);
         assert(success && "FIXME: Unhandled solver failure");
+        (void) success;
         if (result) {
           std::map<BasicBlock*, ref<Expr> >::iterator it =
             targets.insert(std::make_pair(si->getSuccessor(i),
@@ -1419,6 +1428,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       bool res;
       bool success = solver->mayBeTrue(state, isDefault, res);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       if (res)
         targets.insert(std::make_pair(si->getSuccessor(0), isDefault));
       
@@ -1532,6 +1542,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         ref<ConstantExpr> value;
         bool success = solver->getValue(*free, v, value);
         assert(success && "FIXME: Unhandled solver failure");
+        (void) success;
         StatePair res = fork(*free, EqExpr::create(v, value), true);
         if (res.first) {
           void *addr = (void*) (unsigned long) value->getConstantValue();
@@ -2358,6 +2369,7 @@ std::string Executor::getAddressInfo(ExecutionState &state,
     ref<ConstantExpr> value;
     bool success = solver->getValue(state, address, value);
     assert(success && "FIXME: Unhandled solver failure");
+    (void) success;
     example = value->getConstantValue();
     info << "\texample: " << example << "\n";
     std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
@@ -2524,6 +2536,7 @@ void Executor::callExternalFunction(ExecutionState &state,
       ref<ConstantExpr> ce;
       bool success = solver->getValue(state, *ai, ce);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
     } else {
       ref<Expr> arg = toUnique(state, *ai);
@@ -2663,6 +2676,7 @@ void Executor::executeAlloc(ExecutionState &state,
     ref<ConstantExpr> example;
     bool success = solver->getValue(state, size, example);
     assert(success && "FIXME: Unhandled solver failure");
+    (void) success;
     
     // Try and start with a small example
     while (example->getConstantValue() > 128) {
@@ -2672,6 +2686,7 @@ void Executor::executeAlloc(ExecutionState &state,
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
+      (void) success;
       if (!res)
         break;
       example = tmp;
@@ -2684,11 +2699,13 @@ void Executor::executeAlloc(ExecutionState &state,
       ref<ConstantExpr> tmp;
       bool success = solver->getValue(*fixedSize.second, size, tmp);
       assert(success && "FIXME: Unhandled solver failure");      
+      (void) success;
       bool res;
       success = solver->mustBeTrue(*fixedSize.second, 
                                    EqExpr::create(tmp, size),
                                    res);
       assert(success && "FIXME: Unhandled solver failure");      
+      (void) success;
       if (res) {
         executeAlloc(*fixedSize.second, tmp, isLocal,
                      target, zeroMemory, reallocFrom);
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 62aa45db..1e346e89 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -45,6 +45,9 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
   if (numOperands > 2) op3 = evalConstant(ce->getOperand(2));
   
   switch (ce->getOpcode()) {
+    default :
+      assert(0 && "unknown ConstantExpr type");
+
     case Instruction::Trunc: return ExtractExpr::createByteOff(op1, 
 							       0,
 							       Expr::getWidthForLLVMType(type));
@@ -135,9 +138,6 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
     case Instruction::FPToSI:
     case Instruction::FCmp:
       assert(0 && "floating point ConstantExprs unsupported");
-
-    default :
-      assert(0 && "unknown ConstantExpr type");
   }
 }
 
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 5a3af34c..8f144456 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -362,24 +362,24 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
     return read((unsigned) CE->getConstantValue(), width);
   } else { 
     switch (width) {
+    default: assert(0 && "invalid type");
     case  Expr::Bool: return  read1(offset);
     case  Expr::Int8: return  read8(offset);
     case Expr::Int16: return read16(offset);
     case Expr::Int32: return read32(offset);
     case Expr::Int64: return read64(offset);
-    default: assert(0 && "invalid type");
     }
   }
 }
 
 ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
   switch (width) {
+  default: assert(0 && "invalid type");
   case  Expr::Bool: return  read1(offset);
   case  Expr::Int8: return  read8(offset);
   case Expr::Int16: return read16(offset);
   case Expr::Int32: return read32(offset);
   case Expr::Int64: return read64(offset);
-  default: assert(0 && "invalid type");
   }
 }
 
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index cec7b7d1..72c1b67f 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -50,12 +50,14 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, bool isGlobal
 
 MemoryObject *MemoryManager::allocateFixed(uint64_t address, uint64_t size,
                                            const llvm::Value *allocSite) {
+#ifndef NDEBUG
   for (objects_ty::iterator it = objects.begin(), ie = objects.end();
        it != ie; ++it) {
     MemoryObject *mo = *it;
     assert(!(address+size > mo->address && address < mo->address+mo->size) &&
            "allocated an overlapping object");
   }
+#endif
 
   ++stats::allocations;
   MemoryObject *res = new MemoryObject(address, size, false, true, true,
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index f328823b..6fcfe596 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -97,10 +97,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       if (res) {
         ref<ConstantExpr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
+        (void) success;
         it2->second[i] = value->getConstantValue();
         tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
@@ -112,6 +114,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
   bool res;
   bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res);
   assert(success && "FIXME: Unhandled solver failure");
+  (void) success;
   if (res)
     return;
   
@@ -127,10 +130,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
       if (res) {
         ref<ConstantExpr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
+        (void) success;
         it->second[i] = value->getConstantValue();
         tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
@@ -145,6 +150,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     bool success = 
       solver->mayBeTrue(state, assignment.evaluate(condition), res);
     assert(success && "FIXME: Unhandled solver failure");            
+    (void) success;
     assert(res && "seed patching failed");
   }
 #endif
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index d58c9085..57898969 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -41,6 +41,7 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   UpdateList ul(array, true, 0);
 
   switch (w) {
+  default: assert(0 && "invalid width");
   case Expr::Bool: 
     return ZExtExpr::create(ReadExpr::create(ul, 
                                              ConstantExpr::alloc(0,kMachinePointerType)),
@@ -79,7 +80,6 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
                                                 ConstantExpr::alloc(1,kMachinePointerType)),
                                ReadExpr::create(ul, 
                                                 ConstantExpr::alloc(0,kMachinePointerType)));
-  default: assert(0 && "invalid width");
   }
 }
 
@@ -191,8 +191,15 @@ unsigned ReadExpr::computeHash() {
 
 ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
   unsigned numArgs = args.size();
-  
+  (void) numArgs;
+
   switch(k) {
+    case Constant:
+    case Extract:
+    case Read:
+    default:
+      assert(0 && "invalid kind");
+
     case NotOptimized:
       assert(numArgs == 1 && args[0].isExpr() &&
              "invalid args array for given opcode");
@@ -254,14 +261,7 @@ ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
       BINARY_EXPR_CASE(Sle);
       BINARY_EXPR_CASE(Sgt);
       BINARY_EXPR_CASE(Sge);
-
-    case Constant:
-    case Extract:
-    case Read:
-    default:
-      assert(0 && "invalid kind");
   }
-
 }
 
 
@@ -327,23 +327,23 @@ void Expr::print(std::ostream &os) const {
 
 ref<Expr> ConstantExpr::fromMemory(void *address, Width width) {
   switch (width) {
+  default: assert(0 && "invalid type");
   case  Expr::Bool: return ConstantExpr::create(*(( uint8_t*) address), width);
   case  Expr::Int8: return ConstantExpr::create(*(( uint8_t*) address), width);
   case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width);
   case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width);
   case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width);
-  default: assert(0 && "invalid type");
   }
 }
 
 void ConstantExpr::toMemory(void *address) {
   switch (width) {
+  default: assert(0 && "invalid type");
   case  Expr::Bool: *(( uint8_t*) address) = value; break;
   case  Expr::Int8: *(( uint8_t*) address) = value; break;
   case Expr::Int16: *((uint16_t*) address) = value; break;
   case Expr::Int32: *((uint32_t*) address) = value; break;
   case Expr::Int64: *((uint64_t*) address) = value; break;
-  default: assert(0 && "invalid type");
   }
 }
 
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
index c81199d7..cf75974a 100644
--- a/lib/Expr/ExprVisitor.cpp
+++ b/lib/Expr/ExprVisitor.cpp
@@ -91,6 +91,8 @@ ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
     }
 
     switch(res.kind) {
+    default:
+      assert(0 && "invalid kind");
     case Action::DoChildren: {  
       bool rebuild = false;
       ref<Expr> e(&ep), kids[8];
@@ -117,8 +119,6 @@ ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
       return e;
     case Action::ChangeTo:
       return res.argument;
-    default:
-      assert(0 && "invalid kind");
     }
   }
 }
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index f473f70b..a565bab2 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -19,12 +19,12 @@ using namespace llvm;
 IncompleteSolver::PartialValidity 
 IncompleteSolver::negatePartialValidity(PartialValidity pv) {
   switch(pv) {
-    case MustBeTrue:  return MustBeFalse;
-    case MustBeFalse: return MustBeTrue;
-    case MayBeTrue:   return MayBeFalse;
-    case MayBeFalse:  return MayBeTrue;
-    case TrueOrFalse: return TrueOrFalse;
-    default: assert(0 && "invalid partial validity");  
+  default: assert(0 && "invalid partial validity");  
+  case MustBeTrue:  return MustBeFalse;
+  case MustBeFalse: return MustBeTrue;
+  case MayBeTrue:   return MayBeFalse;
+  case MayBeFalse:  return MayBeTrue;
+  case TrueOrFalse: return TrueOrFalse;
   }
 }
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 5b3fdd60..680b7d43 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -92,12 +92,11 @@ STPBuilder::~STPBuilder() {
 
 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];
-  default:
-    assert(0 && "invalid type");
   }
 }
 
@@ -760,8 +759,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 (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
-        assert(!CE->getConstantValue() && "uncanonicalized eq");
+      if (isa<ConstantExpr>(ee->left)) {
+        assert(!cast<ConstantExpr>(ee->left)->getConstantValue() && 
+               "uncanonicalized eq");
         return vc_notExpr(vc, right);
       } else {
         return vc_iffExpr(vc, left, right);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index a673e9e7..936f252d 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -172,7 +172,10 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                                                                           width)),
                                     ConstantExpr::create(0, width))),
                    res);
+
       assert(success && "FIXME: Unhandled solver failure");
+      (void) success;
+
       if (res) {
         hi = mid;
       } else {
@@ -191,7 +194,10 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
       mayBeTrue(query.withExpr(EqExpr::create(e, ConstantExpr::create(0, 
                                                                       width))), 
                 res);
+
     assert(success && "FIXME: Unhandled solver failure");      
+    (void) success;
+
     if (res) {
       min = 0;
     } else {
@@ -205,7 +211,10 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                                                    ConstantExpr::create(mid, 
                                                                         width))),
                     res);
+
         assert(success && "FIXME: Unhandled solver failure");      
+        (void) success;
+
         if (res) {
           hi = mid;
         } else {
@@ -226,7 +235,10 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                                                   ConstantExpr::create(mid, 
                                                                        width))),
                    res);
+
       assert(success && "FIXME: Unhandled solver failure");      
+      (void) success;
+
       if (res) {
         hi = mid;
       } else {