about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Internal/Module/KInstruction.h8
-rw-r--r--lib/Core/Executor.cpp58
-rw-r--r--lib/Core/StatsTracker.cpp45
-rw-r--r--lib/Module/Checks.cpp4
-rw-r--r--lib/Module/InstructionInfoTable.cpp8
-rw-r--r--lib/Module/KInstruction.cpp7
-rw-r--r--lib/Module/KModule.cpp25
-rw-r--r--lib/Module/LowerSwitch.cpp3
-rw-r--r--lib/Module/RaiseAsm.cpp2
-rw-r--r--lib/Solver/CoreSolver.cpp19
-rw-r--r--test/regression/2017-02-21-pathOS-id.c19
-rw-r--r--tools/klee/main.cpp12
12 files changed, 127 insertions, 83 deletions
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index 62f514ff..1cad98fd 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -11,7 +11,11 @@
 #define KLEE_KINSTRUCTION_H
 
 #include "klee/Config/Version.h"
+#include "klee/Internal/Module/InstructionInfoTable.h"
+
 #include "llvm/Support/DataTypes.h"
+#include "llvm/Support/raw_ostream.h"
+
 #include <vector>
 
 namespace llvm {
@@ -39,7 +43,9 @@ namespace klee {
     unsigned dest;
 
   public:
-    virtual ~KInstruction(); 
+    virtual ~KInstruction();
+    void printFileLine(llvm::raw_ostream &);
+
   };
 
   struct KGEPInstruction : KInstruction {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d8a4a32c..95812dd7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -539,7 +539,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
   // ensures that we won't conflict. we don't need to allocate a memory object
   // since reading/writing via a function pointer is unsupported anyway.
   for (Module::iterator i = m->begin(), ie = m->end(); i != ie; ++i) {
-    Function *f = i;
+    Function *f = static_cast<Function *>(i);
     ref<ConstantExpr> addr(0);
 
     // If the symbol has external weak linkage then it is implicitly
@@ -593,7 +593,8 @@ void Executor::initializeGlobals(ExecutionState &state) {
   for (Module::const_global_iterator i = m->global_begin(),
          e = m->global_end();
        i != e; ++i) {
-    size_t globalObjectAlignment = getAllocationAlignment(i);
+    const GlobalVariable *v = static_cast<const GlobalVariable *>(i);
+    size_t globalObjectAlignment = getAllocationAlignment(v);
     if (i->isDeclaration()) {
       // FIXME: We have no general way of handling unknown external
       // symbols. If we really cared about making external stuff work
@@ -626,11 +627,11 @@ void Executor::initializeGlobals(ExecutionState &state) {
       }
 
       MemoryObject *mo = memory->allocate(size, /*isLocal=*/false,
-                                          /*isGlobal=*/true, /*allocSite=*/i,
+                                          /*isGlobal=*/true, /*allocSite=*/v,
                                           /*alignment=*/globalObjectAlignment);
       ObjectState *os = bindObjectInState(state, mo, false);
-      globalObjects.insert(std::make_pair(i, mo));
-      globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));
+      globalObjects.insert(std::make_pair(v, mo));
+      globalAddresses.insert(std::make_pair(v, mo->getBaseExpr()));
 
       // Program already running = object already initialized.  Read
       // concrete value and write it to our copy.
@@ -652,13 +653,13 @@ void Executor::initializeGlobals(ExecutionState &state) {
       LLVM_TYPE_Q Type *ty = i->getType()->getElementType();
       uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
       MemoryObject *mo = memory->allocate(size, /*isLocal=*/false,
-                                          /*isGlobal=*/true, /*allocSite=*/&*i,
+                                          /*isGlobal=*/true, /*allocSite=*/v,
                                           /*alignment=*/globalObjectAlignment);
       if (!mo)
         llvm::report_fatal_error("out of memory");
       ObjectState *os = bindObjectInState(state, mo, false);
-      globalObjects.insert(std::make_pair(i, mo));
-      globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));
+      globalObjects.insert(std::make_pair(v, mo));
+      globalAddresses.insert(std::make_pair(v, mo->getBaseExpr()));
 
       if (!i->hasInitializer())
           os->initializeToRandom();
@@ -670,7 +671,8 @@ void Executor::initializeGlobals(ExecutionState &state) {
        i != ie; ++i) {
     // Map the alias to its aliasee's address. This works because we have
     // addresses for everything, even undefined functions. 
-    globalAddresses.insert(std::make_pair(i, evalConstant(i->getAliasee())));
+    globalAddresses.insert(std::make_pair(static_cast<GlobalAlias *>(i),
+	  evalConstant(i->getAliasee())));
   }
 
   // once all objects are allocated, do the actual initialization
@@ -678,7 +680,8 @@ void Executor::initializeGlobals(ExecutionState &state) {
          e = m->global_end();
        i != e; ++i) {
     if (i->hasInitializer()) {
-      MemoryObject *mo = globalObjects.find(i)->second;
+      const GlobalVariable *v = static_cast<const GlobalVariable *>(i);
+      MemoryObject *mo = globalObjects.find(v)->second;
       const ObjectState *os = state.addressSpace.findObject(mo);
       assert(os);
       ObjectState *wos = state.addressSpace.getWriteable(mo, os);
@@ -973,14 +976,18 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     falseState->ptreeNode = res.first;
     trueState->ptreeNode = res.second;
 
-    if (!isInternal) {
-      if (pathWriter) {
-        falseState->pathOS = pathWriter->open(current.pathOS);
+    if (pathWriter) {
+      // Need to update the pathOS.id field of falseState, otherwise the same id
+      // is used for both falseState and trueState.
+      falseState->pathOS = pathWriter->open(current.pathOS);
+      if (!isInternal) {
         trueState->pathOS << "1";
         falseState->pathOS << "0";
-      }      
-      if (symPathWriter) {
-        falseState->symPathOS = symPathWriter->open(current.symPathOS);
+      }
+    }
+    if (symPathWriter) {
+      falseState->symPathOS = symPathWriter->open(current.symPathOS);
+      if (!isInternal) {
         trueState->symPathOS << "1";
         falseState->symPathOS << "0";
       }
@@ -1232,8 +1239,11 @@ void Executor::printDebugInstructions(ExecutionState &state) {
     stream = &debugLogBuffer;
 
   if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) &&
-      !optionIsSet(DebugPrintInstructions, FILE_COMPACT))
-    printFileLine(state, state.pc, *stream);
+      !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) {
+    (*stream) << "     ";
+    state.pc->printFileLine(*stream);
+    (*stream) << ":";
+  }
 
   (*stream) << state.pc->info->id;
 
@@ -1458,15 +1468,6 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
   }
 }
 
-void Executor::printFileLine(ExecutionState &state, KInstruction *ki,
-                             llvm::raw_ostream &debugFile) {
-  const InstructionInfo &ii = *ki->info;
-  if (ii.file != "")
-    debugFile << "     " << ii.file << ":" << ii.line << ":";
-  else
-    debugFile << "     [no debug info]:";
-}
-
 /// Compute the true target of a function call, resolving LLVM and KLEE aliases
 /// and bitcasts.
 Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
@@ -3543,10 +3544,11 @@ void Executor::runFunctionAsMain(Function *f,
   if (ai!=ae) {
     arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
     if (++ai!=ae) {
+      Instruction *first = static_cast<Instruction *>(f->begin()->begin());
       argvMO =
           memory->allocate((argc + 1 + envc + 1 + 1) * NumPtrBytes,
                            /*isLocal=*/false, /*isGlobal=*/true,
-                           /*allocSite=*/f->begin()->begin(), /*alignment=*/8);
+                           /*allocSite=*/first, /*alignment=*/8);
 
       if (!argvMO)
         klee_error("Could not allocate memory for function arguments");
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index dbd86524..ccf6e04d 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -165,7 +165,7 @@ static bool instructionIsCoverable(Instruction *i) {
     if (it==bb->begin()) {
       return true;
     } else {
-      Instruction *prev = --it;
+      Instruction *prev = static_cast<Instruction *>(--it);
       if (isa<CallInst>(prev) || isa<InvokeInst>(prev)) {
         Function *target =
             getDirectCallTarget(prev, /*moduleIsFullyLinked=*/true);
@@ -539,7 +539,8 @@ void StatsTracker::writeIStats() {
       // Always try to write the filename before the function name, as otherwise
       // KCachegrind can create two entries for the function, one with an
       // unnamed file and one without.
-      const InstructionInfo &ii = executor.kmodule->infos->getFunctionInfo(fnIt);
+      Function *fn = static_cast<Function *>(fnIt);
+      const InstructionInfo &ii = executor.kmodule->infos->getFunctionInfo(fn);
       if (ii.file != sourceFile) {
         of << "fl=" << ii.file << "\n";
         sourceFile = ii.file;
@@ -635,9 +636,9 @@ static std::vector<Instruction*> getSuccs(Instruction *i) {
 
   if (i==bb->getTerminator()) {
     for (succ_iterator it = succ_begin(bb), ie = succ_end(bb); it != ie; ++it)
-      res.push_back(it->begin());
+      res.push_back(static_cast<Instruction *>(it->begin()));
   } else {
-    res.push_back(++BasicBlock::iterator(i));
+    res.push_back(static_cast<Instruction *>(++BasicBlock::iterator(i)));
   }
 
   return res;
@@ -684,18 +685,19 @@ void StatsTracker::computeReachableUncovered() {
            bbIt != bb_ie; ++bbIt) {
         for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
              it != ie; ++it) {
-          if (isa<CallInst>(it) || isa<InvokeInst>(it)) {
-            CallSite cs(it);
+          Instruction *inst = static_cast<Instruction *>(it);
+          if (isa<CallInst>(inst) || isa<InvokeInst>(inst)) {
+            CallSite cs(inst);
             if (isa<InlineAsm>(cs.getCalledValue())) {
               // We can never call through here so assume no targets
               // (which should be correct anyhow).
-              callTargets.insert(std::make_pair(it,
+              callTargets.insert(std::make_pair(inst,
                                                 std::vector<Function*>()));
             } else if (Function *target = getDirectCallTarget(
                            cs, /*moduleIsFullyLinked=*/true)) {
-              callTargets[it].push_back(target);
+              callTargets[inst].push_back(target);
             } else {
-              callTargets[it] = 
+              callTargets[inst] =
                 std::vector<Function*>(km->escapingFunctions.begin(),
                                        km->escapingFunctions.end());
             }
@@ -716,14 +718,15 @@ void StatsTracker::computeReachableUncovered() {
     std::vector<Instruction *> instructions;
     for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
          fnIt != fn_ie; ++fnIt) {
+      Function *fn = static_cast<Function *>(fnIt);
       if (fnIt->isDeclaration()) {
         if (fnIt->doesNotReturn()) {
-          functionShortestPath[fnIt] = 0;
+          functionShortestPath[fn] = 0;
         } else {
-          functionShortestPath[fnIt] = 1; // whatever
+          functionShortestPath[fn] = 1; // whatever
         }
       } else {
-        functionShortestPath[fnIt] = 0;
+        functionShortestPath[fn] = 0;
       }
 
       // Not sure if I should bother to preorder here. XXX I should.
@@ -731,13 +734,14 @@ void StatsTracker::computeReachableUncovered() {
            bbIt != bb_ie; ++bbIt) {
         for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
              it != ie; ++it) {
-          instructions.push_back(it);
-          unsigned id = infos.getInfo(it).id;
+          Instruction *inst = static_cast<Instruction *>(it);
+          instructions.push_back(inst);
+          unsigned id = infos.getInfo(inst).id;
           sm.setIndexedValue(stats::minDistToReturn, 
                              id, 
-                             isa<ReturnInst>(it)
+                             isa<ReturnInst>(inst)
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 1)
-                             || isa<UnwindInst>(it)
+                             || isa<UnwindInst>(inst)
 #endif
                              );
         }
@@ -790,13 +794,13 @@ void StatsTracker::computeReachableUncovered() {
           // that no return instructions are reachable)
           Function *f = inst->getParent()->getParent();
           if (best != cur
-              || (inst == f->begin()->begin()
+              || (inst == static_cast<Instruction *>(f->begin()->begin())
                   && functionShortestPath[f] != best)) {
             sm.setIndexedValue(stats::minDistToReturn, id, best);
             changed = true;
 
             // Update shortest path if this is the entry point.
-            if (inst==f->begin()->begin())
+            if (inst == static_cast<Instruction *>(f->begin()->begin()))
               functionShortestPath[f] = best;
           }
         }
@@ -813,8 +817,9 @@ void StatsTracker::computeReachableUncovered() {
          bbIt != bb_ie; ++bbIt) {
       for (BasicBlock::iterator it = bbIt->begin(), ie = bbIt->end(); 
            it != ie; ++it) {
-        unsigned id = infos.getInfo(it).id;
-        instructions.push_back(&*it);
+        Instruction *inst = static_cast<Instruction *>(it);
+        unsigned id = infos.getInfo(inst).id;
+        instructions.push_back(inst);
         sm.setIndexedValue(stats::minDistToUncovered, 
                            id, 
                            sm.getIndexedValue(stats::uncoveredInstructions, id));
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 44b35e6e..48a4eb94 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -71,7 +71,7 @@ bool DivCheckPass::runOnModule(Module &M) {
                                           Type::getInt64Ty(ctx),
                                           false,  /* sign doesn't matter */
                                           "int_cast_to_i64",
-                                          i);
+                                          static_cast<Instruction *>(i));
             
             // Lazily bind the function to avoid always importing it.
             if (!divZeroCheckFunction) {
@@ -129,7 +129,7 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
                                           Type::getInt64Ty(ctx),
                                           false,  /* sign doesn't matter */
                                           "int_cast_to_i64",
-                                          i);
+                                          static_cast<Instruction *>(i));
             args.push_back(shift);
 
 
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 7e9a9e26..adf05442 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -120,6 +120,7 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
 
   for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
        fnIt != fn_ie; ++fnIt) {
+    Function *fn = static_cast<Function *>(fnIt);
 
     // We want to ensure that as all instructions have source information, if
     // available. Clang sometimes will not write out debug information on the
@@ -128,15 +129,14 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
     // if any.
     const std::string *initialFile = &dummyString;
     unsigned initialLine = 0;
-    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie;
-         ++it) {
+    for (inst_iterator it = inst_begin(fn), ie = inst_end(fn); it != ie; ++it) {
       if (getInstructionDebugInfo(&*it, initialFile, initialLine))
         break;
     }
 
     const std::string *file = initialFile;
     unsigned line = initialLine;
-    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie;
+    for (inst_iterator it = inst_begin(fn), ie = inst_end(fn); it != ie;
         ++it) {
       Instruction *instr = &*it;
       unsigned assemblyLine = lineTable[instr];
@@ -193,6 +193,6 @@ InstructionInfoTable::getFunctionInfo(const Function *f) const {
     // and construct a test case for it if it does, though.
     return dummyInfo;
   } else {
-    return getInfo(f->begin()->begin());
+    return getInfo(static_cast<const Instruction *>(f->begin()->begin()));
   }
 }
diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index 799620c6..a32745b8 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -17,3 +17,10 @@ using namespace klee;
 KInstruction::~KInstruction() {
   delete[] operands;
 }
+
+void KInstruction::printFileLine(llvm::raw_ostream &debugFile) {
+  if (info->file != "")
+    debugFile << info->file << ":" << info->line;
+  else
+    debugFile << "[no debug info]";
+}
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 3259873e..08ec28ef 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -190,7 +190,7 @@ static void injectStaticConstructorsAndDestructors(Module *m) {
 
     if (ctors)
     CallInst::Create(getStubFunctionForCtorList(m, ctors, "klee.ctor_stub"),
-		     "", mainFn->begin()->begin());
+		     "", static_cast<Instruction *>(mainFn->begin()->begin()));
     if (dtors) {
       Function *dtorStub = getStubFunctionForCtorList(m, dtors, "klee.dtor_stub");
       for (Function::iterator it = mainFn->begin(), ie = mainFn->end();
@@ -280,14 +280,15 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
       llvm::errs() << "KLEE: adding klee_merge at exit of: " << name << "\n";
       for (llvm::Function::iterator bbit = f->begin(), bbie = f->end(); 
            bbit != bbie; ++bbit) {
-        if (&*bbit != exit) {
+	BasicBlock *bb = static_cast<BasicBlock *>(bbit);
+        if (bb != exit) {
           Instruction *i = bbit->getTerminator();
           if (i->getOpcode()==Instruction::Ret) {
             if (result) {
-              result->addIncoming(i->getOperand(0), bbit);
+              result->addIncoming(i->getOperand(0), bb);
             }
             i->eraseFromParent();
-	    BranchInst::Create(exit, bbit);
+	    BranchInst::Create(exit, bb);
           }
         }
       }
@@ -444,7 +445,8 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     if (it->isDeclaration())
       continue;
 
-    KFunction *kf = new KFunction(it, this);
+    Function *fn = static_cast<Function *>(it);
+    KFunction *kf = new KFunction(fn, this);
     
     for (unsigned i=0; i<kf->numInstructions; ++i) {
       KInstruction *ki = kf->instructions[i];
@@ -452,7 +454,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     }
 
     functions.push_back(kf);
-    functionMap.insert(std::make_pair(it, kf));
+    functionMap.insert(std::make_pair(fn, kf));
   }
 
   /* Compute various interesting properties */
@@ -529,7 +531,7 @@ KFunction::KFunction(llvm::Function *_function,
     trackCoverage(true) {
   for (llvm::Function::iterator bbit = function->begin(), 
          bbie = function->end(); bbit != bbie; ++bbit) {
-    BasicBlock *bb = bbit;
+    BasicBlock *bb = static_cast<BasicBlock *>(bbit);
     basicBlockEntry[bb] = numInstructions;
     numInstructions += bb->size();
   }
@@ -544,7 +546,7 @@ KFunction::KFunction(llvm::Function *_function,
          bbie = function->end(); bbit != bbie; ++bbit) {
     for (llvm::BasicBlock::iterator it = bbit->begin(), ie = bbit->end();
          it != ie; ++it)
-      registerMap[it] = rnum++;
+      registerMap[static_cast<Instruction *>(it)] = rnum++;
   }
   numRegisters = rnum;
   
@@ -564,11 +566,12 @@ KFunction::KFunction(llvm::Function *_function,
         ki = new KInstruction(); break;
       }
 
-      ki->inst = it;      
-      ki->dest = registerMap[it];
+      Instruction *inst = static_cast<Instruction *>(it);
+      ki->inst = inst;
+      ki->dest = registerMap[inst];
 
       if (isa<CallInst>(it) || isa<InvokeInst>(it)) {
-        CallSite cs(it);
+        CallSite cs(inst);
         unsigned numArgs = cs.arg_size();
         ki->operands = new int[numArgs+1];
         ki->operands[0] = getOperandNum(cs.getCalledValue(), registerMap, km,
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index 7f28748a..5cc6b991 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -44,7 +44,8 @@ bool LowerSwitchPass::runOnFunction(Function &F) {
   bool changed = false;
 
   for (Function::iterator I = F.begin(), E = F.end(); I != E; ) {
-    BasicBlock *cur = I++; // Advance over block so we don't traverse new blocks
+    BasicBlock *cur = static_cast<BasicBlock *>(I);
+    I++; // Advance over block so we don't traverse new blocks
 
     if (SwitchInst *SI = dyn_cast<SwitchInst>(cur->getTerminator())) {
       changed = true;
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index e612ca63..af92b74b 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -115,7 +115,7 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) {
     for (Function::iterator bi = fi->begin(), be = fi->end(); bi != be; ++bi) {
       for (BasicBlock::iterator ii = bi->begin(), ie = bi->end(); ii != ie;) {
-        Instruction *i = ii;
+        Instruction *i = static_cast<Instruction *>(ii);
         ++ii;  
         changed |= runOnInstruction(M, i);
       }
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 783047f8..d36a3219 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -8,6 +8,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/CommandLine.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Solver.h"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/raw_ostream.h"
@@ -51,10 +52,10 @@ static klee::Solver *handleMetaSMT() {
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
   default:
-    llvm_unreachable("Unrecognised metasmt backend");
+    llvm_unreachable("Unrecognised MetaSMT backend");
     break;
   };
-  llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  klee_message("Starting MetaSMTSolver(%s)", backend.c_str());
   return coreSolver;
 }
 #endif /* ENABLE_METASMT */
@@ -65,32 +66,32 @@ Solver *createCoreSolver(CoreSolverType cst) {
   switch (cst) {
   case STP_SOLVER:
 #ifdef ENABLE_STP
-    llvm::errs() << "Using STP solver backend\n";
+    klee_message("Using STP solver backend");
     return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
 #else
-    llvm::errs() << "Not compiled with STP support\n";
+    klee_message("Not compiled with STP support");
     return NULL;
 #endif
   case METASMT_SOLVER:
 #ifdef ENABLE_METASMT
-    llvm::errs() << "Using MetaSMT solver backend\n";
+    klee_message("Using MetaSMT solver backend");
     return handleMetaSMT();
 #else
-    llvm::errs() << "Not compiled with MetaSMT support\n";
+    klee_message("Not compiled with MetaSMT support");
     return NULL;
 #endif
   case DUMMY_SOLVER:
     return createDummySolver();
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
-    llvm::errs() << "Using Z3 solver backend\n";
+    klee_message("Using Z3 solver backend");
     return new Z3Solver();
 #else
-    llvm::errs() << "Not compiled with Z3 support\n";
+    klee_message("Not compiled with Z3 support");
     return NULL;
 #endif
   case NO_SOLVER:
-    llvm::errs() << "Invalid solver\n";
+    klee_message("Invalid solver");
     return NULL;
   default:
     llvm_unreachable("Unsupported CoreSolverType");
diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c
new file mode 100644
index 00000000..d3bffbe0
--- /dev/null
+++ b/test/regression/2017-02-21-pathOS-id.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log
+// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1
+int main(){
+	int a, b;
+	klee_make_symbolic (&a, sizeof(int), "a");
+	klee_make_symbolic (&b, sizeof(int), "b");
+	klee_assume(a<2);
+	klee_assume(a>=0);
+	malloc(a);
+	if(b){
+		b++;//do something
+	}
+	return b;
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 505d259c..c65953d1 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -677,10 +677,10 @@ static int initEnv(Module *mainModule) {
     klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n");
   }
 
-  Instruction* firstInst = mainFn->begin()->begin();
+  Instruction *firstInst = static_cast<Instruction *>(mainFn->begin()->begin());
 
-  Value* oldArgc = mainFn->arg_begin();
-  Value* oldArgv = ++mainFn->arg_begin();
+  Value *oldArgc = static_cast<Argument *>(mainFn->arg_begin());
+  Value *oldArgv = static_cast<Argument *>(++mainFn->arg_begin());
 
   AllocaInst* argcPtr =
     new AllocaInst(oldArgc->getType(), "argcPtr", firstInst);
@@ -1082,7 +1082,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   // naming conflict.
   for (Module::iterator fi = mainModule->begin(), fe = mainModule->end();
        fi != fe; ++fi) {
-    Function *f = fi;
+    Function *f = static_cast<Function *>(fi);
     const std::string &name = f->getName();
     if (name[0]=='\01') {
       unsigned size = name.size();
@@ -1141,8 +1141,8 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   std::vector<llvm::Value*> args;
   args.push_back(llvm::ConstantExpr::getBitCast(userMainFn,
                                                 ft->getParamType(0)));
-  args.push_back(stub->arg_begin()); // argc
-  args.push_back(++stub->arg_begin()); // argv
+  args.push_back(static_cast<Argument *>(stub->arg_begin())); // argc
+  args.push_back(static_cast<Argument *>(++stub->arg_begin())); // argv
   args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init
   args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini
   args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 01:24:34 +0000