Merge pull request #251 from ret2libc/entryFnParam

Added option to specify a different entry point from main().  Remove some whitespaces.

2 files changed, 159 insertions, 144 deletions

diff --git a/test/Feature/EntryPoint.c b/test/Feature/EntryPoint.c
new file mode 100644
index 00000000..2b6a2c70
--- /dev/null
+++ b/test/Feature/EntryPoint.c
@@ -0,0 +1,11 @@
+// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --entry-point=other_main %t.bc > %t.log
+// RUN: grep "Hello World" %t.log
+
+#include <stdio.h>
+
+int other_main() {
+  printf("Hello World\n");
+  return 0;
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index aba247e7..0a292500 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -72,62 +72,67 @@ namespace {
   InputFile(cl::desc("<input bytecode>"), cl::Positional, cl::init("-"));
 
   cl::opt<std::string>
+  EntryPoint("entry-point",
+               cl::desc("Consider the function with the given name as the entrypoint"),
+               cl::init("main"));
+
+  cl::opt<std::string>
   RunInDir("run-in", cl::desc("Change to the given directory prior to executing"));
 
   cl::opt<std::string>
   Environ("environ", cl::desc("Parse environ from given file (in \"env\" format)"));
 
   cl::list<std::string>
-  InputArgv(cl::ConsumeAfter, 
+  InputArgv(cl::ConsumeAfter,
             cl::desc("<program arguments>..."));
 
   cl::opt<bool>
-  NoOutput("no-output", 
+  NoOutput("no-output",
            cl::desc("Don't generate test files"));
-    
+
   cl::opt<bool>
-  WarnAllExternals("warn-all-externals", 
+  WarnAllExternals("warn-all-externals",
                    cl::desc("Give initial warning for all externals."));
-    
+
   cl::opt<bool>
-  WriteCVCs("write-cvcs", 
+  WriteCVCs("write-cvcs",
             cl::desc("Write .cvc files for each test case"));
 
   cl::opt<bool>
-  WritePCs("write-pcs", 
+  WritePCs("write-pcs",
             cl::desc("Write .pc files for each test case"));
-  
+
   cl::opt<bool>
   WriteSMT2s("write-smt2s",
             cl::desc("Write .smt2 (SMT-LIBv2) files for each test case"));
 
   cl::opt<bool>
-  WriteCov("write-cov", 
+  WriteCov("write-cov",
            cl::desc("Write coverage information for each test case"));
-  
+
   cl::opt<bool>
-  WriteTestInfo("write-test-info", 
+  WriteTestInfo("write-test-info",
                 cl::desc("Write additional test case information"));
-  
+
   cl::opt<bool>
-  WritePaths("write-paths", 
+  WritePaths("write-paths",
                 cl::desc("Write .path files for each test case"));
-    
+
   cl::opt<bool>
-  WriteSymPaths("write-sym-paths", 
+  WriteSymPaths("write-sym-paths",
                 cl::desc("Write .sym.path files for each test case"));
-    
+
   cl::opt<bool>
-  ExitOnError("exit-on-error", 
+  ExitOnError("exit-on-error",
               cl::desc("Exit if errors occur"));
-    
+
 
   enum LibcType {
     NoLibc, KleeLibc, UcLibc
   };
 
   cl::opt<LibcType>
-  Libc("libc", 
+  Libc("libc",
        cl::desc("Choose libc version (none by default)."),
        cl::values(clEnumValN(NoLibc, "none", "Don't link in a libc"),
                   clEnumValN(KleeLibc, "klee", "Link in klee libc"),
@@ -135,19 +140,19 @@ namespace {
 		  clEnumValEnd),
        cl::init(NoLibc));
 
-    
+
   cl::opt<bool>
-  WithPOSIXRuntime("posix-runtime", 
+  WithPOSIXRuntime("posix-runtime",
 		cl::desc("Link with POSIX runtime.  Options that can be passed as arguments to the programs are: --sym-argv <max-len>  --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options"),
 		cl::init(false));
-    
+
   cl::opt<bool>
-  OptimizeModule("optimize", 
+  OptimizeModule("optimize",
                  cl::desc("Optimize before execution"),
 		 cl::init(false));
 
   cl::opt<bool>
-  CheckDivZero("check-div-zero", 
+  CheckDivZero("check-div-zero",
                cl::desc("Inject checks for division-by-zero"),
                cl::init(true));
 
@@ -157,15 +162,15 @@ namespace {
                cl::init(true));
 
   cl::opt<std::string>
-  OutputDir("output-dir", 
+  OutputDir("output-dir",
             cl::desc("Directory to write results in (defaults to klee-out-N)"),
             cl::init(""));
 
   cl::opt<bool>
-  ReplayKeepSymbolic("replay-keep-symbolic", 
+  ReplayKeepSymbolic("replay-keep-symbolic",
                      cl::desc("Replay the test cases only by asserting "
                               "the bytes, not necessarily making them concrete."));
-    
+
   cl::list<std::string>
   ReplayOutFile("replay-out",
                 cl::desc("Specify an out file to replay"),
@@ -183,17 +188,17 @@ namespace {
 
   cl::list<std::string>
   SeedOutFile("seed-out");
-  
+
   cl::list<std::string>
   SeedOutDir("seed-out-dir");
-  
+
   cl::opt<unsigned>
   MakeConcreteSymbolic("make-concrete-symbolic",
                        cl::desc("Probabilistic rate at which to make concrete reads symbolic, "
 				"i.e. approximately 1 in n concrete reads will be made symbolic (0=off, 1=all).  "
 				"Used for testing."),
                        cl::init(0));
- 
+
   cl::opt<unsigned>
   StopAfterNTests("stop-after-n-tests",
 	     cl::desc("Stop execution after generating the given number of tests.  Extra tests corresponding to partially explored paths will also be dumped."),
@@ -236,7 +241,7 @@ public:
   void setInterpreter(Interpreter *i);
 
   void processTestCase(const ExecutionState  &state,
-                       const char *errorMessage, 
+                       const char *errorMessage,
                        const char *errorSuffix);
 
   std::string getOutputFilename(const std::string &filename);
@@ -245,11 +250,11 @@ public:
   llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id);
 
   // load a .out file
-  static void loadOutFile(std::string name, 
+  static void loadOutFile(std::string name,
                           std::vector<unsigned char> &buffer);
 
   // load a .path file
-  static void loadPathFile(std::string name, 
+  static void loadPathFile(std::string name,
                            std::vector<bool> &buffer);
 
   static void getOutFiles(std::string path,
@@ -258,7 +263,7 @@ public:
   static std::string getRunTimeLibraryPath(const char *argv0);
 };
 
-KleeHandler::KleeHandler(int argc, char **argv) 
+KleeHandler::KleeHandler(int argc, char **argv)
   : m_interpreter(0),
     m_pathWriter(0),
     m_symPathWriter(0),
@@ -404,7 +409,7 @@ llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix,
 
 /* Outputs all files (.ktest, .pc, .cov etc.) describing a test case */
 void KleeHandler::processTestCase(const ExecutionState &state,
-                                  const char *errorMessage, 
+                                  const char *errorMessage,
                                   const char *errorSuffix) {
   if (errorMessage && ExitOnError) {
     llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n";
@@ -423,7 +428,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     unsigned id = ++m_testIndex;
 
     if (success) {
-      KTest b;      
+      KTest b;
       b.numArgs = m_argc;
       b.args = m_argv;
       b.symArgvs = 0;
@@ -439,11 +444,11 @@ void KleeHandler::processTestCase(const ExecutionState &state,
         assert(o->bytes);
         std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
       }
-      
+
       if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) {
         klee_warning("unable to write output test case, losing it");
       }
-      
+
       for (unsigned i=0; i<b.numObjects; i++)
         delete[] b.objects[i].bytes;
       delete[] b.objects;
@@ -454,7 +459,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       *f << errorMessage;
       delete f;
     }
-    
+
     if (m_pathWriter) {
       std::vector<unsigned char> concreteBranches;
       m_pathWriter->readStream(m_interpreter->getPathStreamID(state),
@@ -467,7 +472,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       }
       delete f;
     }
-   
+
     if (errorMessage || WritePCs) {
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
@@ -483,9 +488,9 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       *f << constraints;
       delete f;
     }
-    
+
     if(WriteSMT2s) {
-    	std::string constraints;
+      std::string constraints;
         m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
         llvm::raw_ostream *f = openTestFile("smt2", id);
         *f << constraints;
@@ -524,7 +529,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     if (WriteTestInfo) {
       double elapsed_time = util::getWallTime() - start_time;
       llvm::raw_ostream *f = openTestFile("info", id);
-      *f << "Time to generate test case: " 
+      *f << "Time to generate test case: "
          << elapsed_time << "s\n";
       delete f;
     }
@@ -532,7 +537,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 }
 
   // load a .path file
-void KleeHandler::loadPathFile(std::string name, 
+void KleeHandler::loadPathFile(std::string name,
                                      std::vector<bool> &buffer) {
   std::ifstream f(name.c_str(), std::ios::in | std::ios::binary);
 
@@ -647,8 +652,8 @@ static int initEnv(Module *mainModule) {
     oldArgv->replaceAllUsesWith(nArgv)
   */
 
-  Function *mainFn = mainModule->getFunction("main");
-    
+  Function *mainFn = mainModule->getFunction(EntryPoint);
+
   if (mainFn->arg_size() < 2) {
     klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n");
   }
@@ -657,23 +662,23 @@ static int initEnv(Module *mainModule) {
 
   Value* oldArgc = mainFn->arg_begin();
   Value* oldArgv = ++mainFn->arg_begin();
-  
-  AllocaInst* argcPtr = 
+
+  AllocaInst* argcPtr =
     new AllocaInst(oldArgc->getType(), "argcPtr", firstInst);
-  AllocaInst* argvPtr = 
+  AllocaInst* argvPtr =
     new AllocaInst(oldArgv->getType(), "argvPtr", firstInst);
 
   /* Insert void klee_init_env(int* argc, char*** argv) */
   std::vector<const Type*> params;
   params.push_back(Type::getInt32Ty(getGlobalContext()));
   params.push_back(Type::getInt32Ty(getGlobalContext()));
-  Function* initEnvFn = 
+  Function* initEnvFn =
     cast<Function>(mainModule->getOrInsertFunction("klee_init_env",
                                                    Type::getVoidTy(getGlobalContext()),
                                                    argcPtr->getType(),
                                                    argvPtr->getType(),
                                                    NULL));
-  assert(initEnvFn);    
+  assert(initEnvFn);
   std::vector<Value*> args;
   args.push_back(argcPtr);
   args.push_back(argvPtr);
@@ -681,12 +686,12 @@ static int initEnv(Module *mainModule) {
   Instruction* initEnvCall = CallInst::Create(initEnvFn, args,
 					      "", firstInst);
 #else
-  Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(), 
+  Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(),
 					      "", firstInst);
 #endif
   Value *argc = new LoadInst(argcPtr, "newArgc", firstInst);
   Value *argv = new LoadInst(argvPtr, "newArgv", firstInst);
-  
+
   oldArgc->replaceAllUsesWith(argc);
   oldArgv->replaceAllUsesWith(argv);
 
@@ -708,54 +713,54 @@ static const char *modelledExternals[] = {
   "_ZTVN10__cxxabiv121__vmi_class_type_infoE",
 
   // special functions
-  "_assert", 
-  "__assert_fail", 
-  "__assert_rtn", 
-  "calloc", 
-  "_exit", 
-  "exit", 
-  "free", 
-  "abort", 
-  "klee_abort", 
-  "klee_assume", 
+  "_assert",
+  "__assert_fail",
+  "__assert_rtn",
+  "calloc",
+  "_exit",
+  "exit",
+  "free",
+  "abort",
+  "klee_abort",
+  "klee_assume",
   "klee_check_memory_access",
   "klee_define_fixed_object",
-  "klee_get_errno", 
+  "klee_get_errno",
   "klee_get_valuef",
   "klee_get_valued",
   "klee_get_valuel",
   "klee_get_valuell",
   "klee_get_value_i32",
   "klee_get_value_i64",
-  "klee_get_obj_size", 
-  "klee_is_symbolic", 
-  "klee_make_symbolic", 
-  "klee_mark_global", 
-  "klee_merge", 
+  "klee_get_obj_size",
+  "klee_is_symbolic",
+  "klee_make_symbolic",
+  "klee_mark_global",
+  "klee_merge",
   "klee_prefer_cex",
-  "klee_print_expr", 
-  "klee_print_range", 
-  "klee_report_error", 
+  "klee_print_expr",
+  "klee_print_range",
+  "klee_report_error",
   "klee_set_forking",
-  "klee_silent_exit", 
-  "klee_warning", 
-  "klee_warning_once", 
+  "klee_silent_exit",
+  "klee_warning",
+  "klee_warning_once",
   "klee_alias_function",
   "klee_stack_trace",
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
   "llvm.dbg.declare",
   "llvm.dbg.value",
 #endif
-  "llvm.va_start", 
-  "llvm.va_end", 
-  "malloc", 
-  "realloc", 
-  "_ZdaPv", 
-  "_ZdlPv", 
-  "_Znaj", 
-  "_Znwj", 
-  "_Znam", 
-  "_Znwm", 
+  "llvm.va_start",
+  "llvm.va_end",
+  "malloc",
+  "realloc",
+  "_ZdaPv",
+  "_ZdlPv",
+  "_Znaj",
+  "_Znwj",
+  "_Znam",
+  "_Znwm",
   "__ubsan_handle_add_overflow",
   "__ubsan_handle_sub_overflow",
   "__ubsan_handle_mul_overflow",
@@ -804,7 +809,7 @@ static const char *dontCareExternals[] = {
   "uname",
 
   // fp stuff we just don't worry about yet
-  "frexp",  
+  "frexp",
   "ldexp",
   "__isnan",
   "__signbit",
@@ -840,15 +845,15 @@ static const char *unsafeExternals[] = {
 #define NELEMS(array) (sizeof(array)/sizeof(array[0]))
 void externalsAndGlobalsCheck(const Module *m) {
   std::map<std::string, bool> externals;
-  std::set<std::string> modelled(modelledExternals, 
+  std::set<std::string> modelled(modelledExternals,
                                  modelledExternals+NELEMS(modelledExternals));
-  std::set<std::string> dontCare(dontCareExternals, 
+  std::set<std::string> dontCare(dontCareExternals,
                                  dontCareExternals+NELEMS(dontCareExternals));
-  std::set<std::string> unsafe(unsafeExternals, 
+  std::set<std::string> unsafe(unsafeExternals,
                                unsafeExternals+NELEMS(unsafeExternals));
 
   switch (Libc) {
-  case KleeLibc: 
+  case KleeLibc:
     dontCare.insert(dontCareKlee, dontCareKlee+NELEMS(dontCareKlee));
     break;
   case UcLibc:
@@ -858,40 +863,39 @@ void externalsAndGlobalsCheck(const Module *m) {
   case NoLibc: /* silence compiler warning */
     break;
   }
-  
 
   if (WithPOSIXRuntime)
     dontCare.insert("syscall");
 
-  for (Module::const_iterator fnIt = m->begin(), fn_ie = m->end(); 
+  for (Module::const_iterator fnIt = m->begin(), fn_ie = m->end();
        fnIt != fn_ie; ++fnIt) {
     if (fnIt->isDeclaration() && !fnIt->use_empty())
       externals.insert(std::make_pair(fnIt->getName(), false));
-    for (Function::const_iterator bbIt = fnIt->begin(), bb_ie = fnIt->end(); 
+    for (Function::const_iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
          bbIt != bb_ie; ++bbIt) {
-      for (BasicBlock::const_iterator it = bbIt->begin(), ie = bbIt->end(); 
+      for (BasicBlock::const_iterator it = bbIt->begin(), ie = bbIt->end();
            it != ie; ++it) {
         if (const CallInst *ci = dyn_cast<CallInst>(it)) {
           if (isa<InlineAsm>(ci->getCalledValue())) {
             klee_warning_once(&*fnIt,
-                              "function \"%s\" has inline asm", 
+                              "function \"%s\" has inline asm",
                               fnIt->getName().data());
           }
         }
       }
     }
   }
-  for (Module::const_global_iterator 
-         it = m->global_begin(), ie = m->global_end(); 
+  for (Module::const_global_iterator
+         it = m->global_begin(), ie = m->global_end();
        it != ie; ++it)
     if (it->isDeclaration() && !it->use_empty())
       externals.insert(std::make_pair(it->getName(), true));
   // and remove aliases (they define the symbol after global
   // initialization)
-  for (Module::const_alias_iterator 
-         it = m->alias_begin(), ie = m->alias_end(); 
+  for (Module::const_alias_iterator
+         it = m->alias_begin(), ie = m->alias_end();
        it != ie; ++it) {
-    std::map<std::string, bool>::iterator it2 = 
+    std::map<std::string, bool>::iterator it2 =
       externals.find(it->getName());
     if (it2!=externals.end())
       externals.erase(it2);
@@ -902,7 +906,7 @@ void externalsAndGlobalsCheck(const Module *m) {
          it = externals.begin(), ie = externals.end();
        it != ie; ++it) {
     const std::string &ext = it->first;
-    if (!modelled.count(ext) && (WarnAllExternals || 
+    if (!modelled.count(ext) && (WarnAllExternals ||
                                  !dontCare.count(ext))) {
       if (unsafe.count(ext)) {
         foundUnsafe.insert(*it);
@@ -962,12 +966,12 @@ static void interrupt_handle_watchdog() {
 // the state data before going ahead and killing it.
 static void halt_via_gdb(int pid) {
   char buffer[256];
-  sprintf(buffer, 
+  sprintf(buffer,
           "gdb --batch --eval-command=\"p halt_execution()\" "
           "--eval-command=detach --pid=%d &> /dev/null",
           pid);
   //  fprintf(stderr, "KLEE: WATCHDOG: running: %s\n", buffer);
-  if (system(buffer)==-1) 
+  if (system(buffer)==-1)
     perror("system");
 }
 
@@ -1025,7 +1029,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
                                   FunctionType::get(Type::getVoidTy(getGlobalContext()),
                                                std::vector<LLVM_TYPE_Q Type*>(),
                                                     true));
-  
+
   // force various imports
   if (WithPOSIXRuntime) {
     LLVM_TYPE_Q llvm::Type *i8Ty = Type::getInt8Ty(getGlobalContext());
@@ -1075,7 +1079,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
       }
     }
   }
-  
+
   mainModule = klee::linkWithLibrary(mainModule, uclibcBCA.c_str());
   assert(mainModule && "unable to link with uclibc");
 
@@ -1096,10 +1100,10 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   // also an implicit cooperation in that runFunctionAsMain sets up
   // the environment arguments to what uclibc expects (following
   // argv), since it does not explicitly take an envp argument.
-  Function *userMainFn = mainModule->getFunction("main");
-  assert(userMainFn && "unable to get user main");    
+  Function *userMainFn = mainModule->getFunction(EntryPoint);
+  assert(userMainFn && "unable to get user main");
   Function *uclibcMainFn = mainModule->getFunction("__uClibc_main");
-  assert(uclibcMainFn && "unable to get uclibc main");    
+  assert(uclibcMainFn && "unable to get uclibc main");
   userMainFn->setName("__user_main");
 
   const FunctionType *ft = uclibcMainFn->getFunctionType();
@@ -1109,16 +1113,16 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
   fArgs.push_back(ft->getParamType(1)); // argc
   fArgs.push_back(ft->getParamType(2)); // argv
   Function *stub = Function::Create(FunctionType::get(Type::getInt32Ty(getGlobalContext()), fArgs, false),
-      			      GlobalVariable::ExternalLinkage,
-      			      "main",
-      			      mainModule);
+                                    GlobalVariable::ExternalLinkage,
+                                    EntryPoint,
+                                    mainModule);
   BasicBlock *bb = BasicBlock::Create(getGlobalContext(), "entry", stub);
 
   std::vector<llvm::Value*> args;
-  args.push_back(llvm::ConstantExpr::getBitCast(userMainFn, 
+  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(++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
@@ -1128,7 +1132,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
 #else
   CallInst::Create(uclibcMainFn, args.begin(), args.end(), "", bb);
 #endif
-  
+
   new UnreachableInst(getGlobalContext(), bb);
 
   klee_message("NOTE: Using klee-uclibc : %s", uclibcBCA.c_str());
@@ -1183,7 +1187,7 @@ int main(int argc, char **argv, char **envp) {
 
           if (time > nextStep) {
             ++level;
-            
+
             if (level==1) {
               fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n");
               kill(pid, SIGINT);
@@ -1265,10 +1269,10 @@ int main(int argc, char **argv, char **envp) {
 
   std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]);
   Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
-                                  /*Optimize=*/OptimizeModule, 
+                                  /*Optimize=*/OptimizeModule,
                                   /*CheckDivZero=*/CheckDivZero,
                                   /*CheckOvershift=*/CheckOvershift);
-  
+
   switch (Libc) {
   case NoLibc: /* silence compiler warning */
     break;
@@ -1297,13 +1301,13 @@ int main(int argc, char **argv, char **envp) {
     klee_message("NOTE: Using model: %s", Path.c_str());
     mainModule = klee::linkWithLibrary(mainModule, Path.c_str());
     assert(mainModule && "unable to link with simple model");
-  }  
+  }
 
   // Get the desired main function.  klee_main initializes uClibc
   // locale and other data and then calls main.
-  Function *mainFn = mainModule->getFunction("main");
+  Function *mainFn = mainModule->getFunction(EntryPoint);
   if (!mainFn) {
-    llvm::errs() << "'main' function not found in module.\n";
+    llvm::errs() << "'" << EntryPoint << "' function not found in module.\n";
     return -1;
   }
 
@@ -1333,16 +1337,16 @@ int main(int argc, char **argv, char **envp) {
     pEnvp = envp;
   }
 
-  pArgc = InputArgv.size() + 1; 
+  pArgc = InputArgv.size() + 1;
   pArgv = new char *[pArgc];
   for (unsigned i=0; i<InputArgv.size()+1; i++) {
     std::string &arg = (i==0 ? InputFile : InputArgv[i-1]);
     unsigned size = arg.size() + 1;
     char *pArg = new char[size];
-    
+
     std::copy(arg.begin(), arg.end(), pArg);
     pArg[size - 1] = 0;
-    
+
     pArgv[i] = pArg;
   }
 
@@ -1355,7 +1359,7 @@ int main(int argc, char **argv, char **envp) {
   Interpreter::InterpreterOptions IOpts;
   IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
   KleeHandler *handler = new KleeHandler(pArgc, pArgv);
-  Interpreter *interpreter = 
+  Interpreter *interpreter =
     theInterpreter = Interpreter::create(IOpts, handler);
   handler->setInterpreter(interpreter);
 
@@ -1365,7 +1369,7 @@ int main(int argc, char **argv, char **envp) {
   }
   infoFile << "PID: " << getpid() << "\n";
 
-  const Module *finalModule = 
+  const Module *finalModule =
     interpreter->setModule(mainModule, Opts);
   externalsAndGlobalsCheck(finalModule);
 
@@ -1388,7 +1392,7 @@ int main(int argc, char **argv, char **envp) {
     for (std::vector<std::string>::iterator
            it = ReplayOutDir.begin(), ie = ReplayOutDir.end();
          it != ie; ++it)
-      KleeHandler::getOutFiles(*it, outFiles);    
+      KleeHandler::getOutFiles(*it, outFiles);
     std::vector<KTest*> kTests;
     for (std::vector<std::string>::iterator
            it = outFiles.begin(), ie = outFiles.end();
@@ -1437,7 +1441,7 @@ int main(int argc, char **argv, char **envp) {
         exit(1);
       }
       seeds.push_back(out);
-    } 
+    }
     for (std::vector<std::string>::iterator
            it = SeedOutDir.begin(), ie = SeedOutDir.end();
          it != ie; ++it) {
@@ -1458,7 +1462,7 @@ int main(int argc, char **argv, char **envp) {
         exit(1);
       }
     }
-       
+
     if (!seeds.empty()) {
       llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n";
       interpreter->useSeeds(&seeds);
@@ -1476,7 +1480,7 @@ int main(int argc, char **argv, char **envp) {
       seeds.pop_back();
     }
   }
-      
+
   t[1] = time(NULL);
   strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1]));
   infoFile << buf;
@@ -1492,31 +1496,31 @@ int main(int argc, char **argv, char **envp) {
 
   delete interpreter;
 
-  uint64_t queries = 
+  uint64_t queries =
     *theStatisticManager->getStatisticByName("Queries");
-  uint64_t queriesValid = 
+  uint64_t queriesValid =
     *theStatisticManager->getStatisticByName("QueriesValid");
-  uint64_t queriesInvalid = 
+  uint64_t queriesInvalid =
     *theStatisticManager->getStatisticByName("QueriesInvalid");
-  uint64_t queryCounterexamples = 
+  uint64_t queryCounterexamples =
     *theStatisticManager->getStatisticByName("QueriesCEX");
-  uint64_t queryConstructs = 
+  uint64_t queryConstructs =
     *theStatisticManager->getStatisticByName("QueriesConstructs");
-  uint64_t instructions = 
+  uint64_t instructions =
     *theStatisticManager->getStatisticByName("Instructions");
-  uint64_t forks = 
+  uint64_t forks =
     *theStatisticManager->getStatisticByName("Forks");
 
-  handler->getInfoStream() 
+  handler->getInfoStream()
     << "KLEE: done: explored paths = " << 1 + forks << "\n";
 
   // Write some extra information in the info file which users won't
   // necessarily care about or understand.
   if (queries)
-    handler->getInfoStream() 
-      << "KLEE: done: avg. constructs per query = " 
-                             << queryConstructs / queries << "\n";  
-  handler->getInfoStream() 
+    handler->getInfoStream()
+      << "KLEE: done: avg. constructs per query = "
+                             << queryConstructs / queries << "\n";
+  handler->getInfoStream()
     << "KLEE: done: total queries = " << queries << "\n"
     << "KLEE: done: valid queries = " << queriesValid << "\n"
     << "KLEE: done: invalid queries = " << queriesInvalid << "\n"
@@ -1524,11 +1528,11 @@ int main(int argc, char **argv, char **envp) {
 
   std::stringstream stats;
   stats << "\n";
-  stats << "KLEE: done: total instructions = " 
+  stats << "KLEE: done: total instructions = "
         << instructions << "\n";
-  stats << "KLEE: done: completed paths = " 
+  stats << "KLEE: done: completed paths = "
         << handler->getNumPathsExplored() << "\n";
-  stats << "KLEE: done: generated tests = " 
+  stats << "KLEE: done: generated tests = "
         << handler->getNumTestCases() << "\n";
 
   bool useColors = llvm::errs().is_displayed();