diff options
| -rw-r--r-- | include/klee/Internal/Module/KInstIterator.h | 7 | ||||
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 27 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 310 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 105 | ||||
| -rw-r--r-- | test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery | 15 | ||||
| -rw-r--r-- | test/regression/2016-04-14-sdiv-2.c_ | 25 | ||||
| -rw-r--r-- | test/regression/lit.local.cfg | 2 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 13 |
9 files changed, 279 insertions, 229 deletions
diff --git a/include/klee/Internal/Module/KInstIterator.h b/include/klee/Internal/Module/KInstIterator.h index 88efed38..736c4b4d 100644 --- a/include/klee/Internal/Module/KInstIterator.h +++ b/include/klee/Internal/Module/KInstIterator.h @@ -19,13 +19,6 @@ namespace klee { public: KInstIterator() : it(0) {} KInstIterator(KInstruction **_it) : it(_it) {} - KInstIterator(const KInstIterator &b) : it(b.it) {} - ~KInstIterator() {} - - KInstIterator &operator=(const KInstIterator &b) { - it = b.it; - return *this; - } bool operator==(const KInstIterator &b) const { return it==b.it; diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 1724ea06..a0fbda03 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -61,8 +61,8 @@ UseForkedCoreSolver("use-forked-solver", llvm::cl::opt<bool> CoreSolverOptimizeDivides("solver-optimize-divides", - llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), - llvm::cl::init(true)); + llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"), + llvm::cl::init(false)); /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 78126ede..3594fecf 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -438,23 +438,36 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } - // Helper function used only for assertions to make sure point created -// during computeInitialValues is in fact correct. +// during computeInitialValues is in fact correct. The ``retMap`` is used +// in the case ``objects`` doesn't contain all the assignments needed. bool assertCreatedPointEvaluatesToTrue(const Query &query, const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values){ - Assignment assign = Assignment(objects, values); + std::vector< std::vector<unsigned char> > &values, + std::map<const Array*, std::vector<unsigned char> > &retMap){ + // _allowFreeValues is set to true so that if there are missing bytes in the assigment + // we will end up with a non ConstantExpr after evaluating the assignment and fail + Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); + + // Add any additional bindings. + // The semantics of std::map should be to not insert a (key, value) + // pair if it already exists so we should continue to use the assignment + // from ``objects`` and ``values``. + if (retMap.size() > 0) + assign.bindings.insert(retMap.begin(), retMap.end()); + for(ConstraintManager::constraint_iterator it = query.constraints.begin(); it != query.constraints.end(); ++it){ ref<Expr> ret = assign.evaluate(*it); - if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){ + + assert(isa<ConstantExpr>(ret) && "assignment evaluation did not result in constant"); + ref<ConstantExpr> evaluatedConstraint = dyn_cast<ConstantExpr>(ret); + if(evaluatedConstraint->isFalse()){ return false; } } ref<Expr> neg = Expr::createIsZero(query.expr); ref<Expr> q = assign.evaluate(neg); - assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); return cast<ConstantExpr>(q)->isTrue(); } @@ -529,7 +542,7 @@ bool IndependentSolver::computeInitialValues(const Query& query, values.push_back(retMap[arr]); } } - assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"); + assert(assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && "should satisfy the equation"); delete factors; return true; } diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 5484a319..f93bec3c 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -1,13 +1,4 @@ //===-- QueryLoggingSolver.cpp --------------------------------------------===// - -#include "QueryLoggingSolver.h" -#include "klee/Internal/System/Time.h" -#include "klee/Statistics.h" - -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) -#include "llvm/Support/FileSystem.h" -#endif - // // The KLEE Symbolic Virtual Machine // @@ -15,188 +6,203 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +#include "QueryLoggingSolver.h" +#include "klee/Internal/System/Time.h" +#include "klee/Statistics.h" + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif using namespace klee::util; -QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog) +namespace { +llvm::cl::opt<bool> DumpPartialQueryiesEarly( + "log-partial-queries-early", llvm::cl::init(false), + llvm::cl::desc("Log queries before calling the solver (default=off)")); +} + +QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, + int queryTimeToLog) : solver(_solver), #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), #else os(path.c_str(), ErrorInfo), #endif - BufferString(""), - logBuffer(BufferString), - queryCount(0), - minQueryTimeToLog(queryTimeToLog), - startTime(0.0f), - lastQueryTime(0.0f), + BufferString(""), logBuffer(BufferString), queryCount(0), + minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), queryCommentSign(commentSign) { - assert(0 != solver); + assert(0 != solver); } -QueryLoggingSolver::~QueryLoggingSolver() { - delete solver; +QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } + +void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { + logBuffer.flush(); + if (writeToFile) { + os << logBuffer.str(); + os.flush(); + } + // prepare the buffer for reuse + BufferString = ""; } -void QueryLoggingSolver::startQuery(const Query& query, const char* typeName, - const Query* falseQuery, - const std::vector<const Array*> *objects) { - Statistic *S = theStatisticManager->getStatisticByName("Instructions"); - uint64_t instructions = S ? S->getValue() : 0; - - logBuffer << queryCommentSign << " Query " << queryCount++ << " -- " - << "Type: " << typeName << ", " - << "Instructions: " << instructions << "\n"; - - printQuery(query, falseQuery, objects); - - startTime = getWallTime(); - +void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, + const Query *falseQuery, + const std::vector<const Array *> *objects) { + Statistic *S = theStatisticManager->getStatisticByName("Instructions"); + uint64_t instructions = S ? S->getValue() : 0; + + logBuffer << queryCommentSign << " Query " << queryCount++ << " -- " + << "Type: " << typeName << ", " + << "Instructions: " << instructions << "\n"; + + printQuery(query, falseQuery, objects); + + if (DumpPartialQueryiesEarly) { + flushBufferConditionally(true); + } + startTime = getWallTime(); } void QueryLoggingSolver::finishQuery(bool success) { - lastQueryTime = getWallTime() - startTime; - logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << lastQueryTime << "\n"; - - if (false == success) { - logBuffer << queryCommentSign << " Failure reason: " - << SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode()) - << "\n"; - } + lastQueryTime = getWallTime() - startTime; + logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " + << "Elapsed: " << lastQueryTime << "\n"; + + if (false == success) { + logBuffer << queryCommentSign << " Failure reason: " + << SolverImpl::getOperationStatusString( + solver->impl->getOperationStatusCode()) << "\n"; + } } void QueryLoggingSolver::flushBuffer() { - logBuffer.flush(); - - if ((0 == minQueryTimeToLog) || - (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) { - // we either do not limit logging queries or the query time - // is larger than threshold (in ms) - - if ((minQueryTimeToLog >= 0) || - (SOLVER_RUN_STATUS_TIMEOUT == (solver->impl->getOperationStatusCode()))) { - // we do additional check here to log only timeouts in case - // user specified negative value for minQueryTimeToLog param - os << logBuffer.str(); - os.flush(); - } - } - - // prepare the buffer for reuse - BufferString = ""; + bool writeToFile = false; + + if ((0 == minQueryTimeToLog) || + (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) { + // we either do not limit logging queries or the query time + // is larger than threshold (in ms) + + if ((minQueryTimeToLog >= 0) || + (SOLVER_RUN_STATUS_TIMEOUT == + (solver->impl->getOperationStatusCode()))) { + // we do additional check here to log only timeouts in case + // user specified negative value for minQueryTimeToLog param + writeToFile = true; + } + } + + flushBufferConditionally(writeToFile); } -bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { - startQuery(query, "Truth"); - - bool success = solver->impl->computeTruth(query, isValid); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Is Valid: " - << (isValid ? "true" : "false") << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; +bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) { + startQuery(query, "Truth"); + + bool success = solver->impl->computeTruth(query, isValid); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign + << " Is Valid: " << (isValid ? "true" : "false") << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeValidity(const Query& query, - Solver::Validity& result) { - startQuery(query, "Validity"); - - bool success = solver->impl->computeValidity(query, result); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Validity: " - << result << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; +bool QueryLoggingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + startQuery(query, "Validity"); + + bool success = solver->impl->computeValidity(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Validity: " << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeValue(const Query& query, ref<Expr>& result) { - Query withFalse = query.withFalse(); - startQuery(query, "Value", &withFalse); +bool QueryLoggingSolver::computeValue(const Query &query, ref<Expr> &result) { + Query withFalse = query.withFalse(); + startQuery(query, "Value", &withFalse); - bool success = solver->impl->computeValue(query, result); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Result: " << result << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; + bool success = solver->impl->computeValue(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Result: " << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeInitialValues(const Query& query, - const std::vector<const Array*>& objects, - std::vector<std::vector<unsigned char> >& values, - bool& hasSolution) { - startQuery(query, "InitialValues", 0, &objects); - - bool success = solver->impl->computeInitialValues(query, objects, - values, hasSolution); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Solvable: " - << (hasSolution ? "true" : "false") << "\n"; - if (hasSolution) { - std::vector< std::vector<unsigned char> >::iterator - values_it = values.begin(); - - for (std::vector<const Array*>::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) { - const Array *array = *i; - std::vector<unsigned char> &data = *values_it; - logBuffer << queryCommentSign << " " << array->name << " = ["; - - for (unsigned j = 0; j < array->size; j++) { - logBuffer << (int) data[j]; - - if (j+1 < array->size) { - logBuffer << ","; - } - } - logBuffer << "]\n"; - } +bool QueryLoggingSolver::computeInitialValues( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + startQuery(query, "InitialValues", 0, &objects); + + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign + << " Solvable: " << (hasSolution ? "true" : "false") << "\n"; + if (hasSolution) { + std::vector<std::vector<unsigned char> >::iterator values_it = + values.begin(); + + for (std::vector<const Array *>::const_iterator i = objects.begin(), + e = objects.end(); + i != e; ++i, ++values_it) { + const Array *array = *i; + std::vector<unsigned char> &data = *values_it; + logBuffer << queryCommentSign << " " << array->name << " = ["; + + for (unsigned j = 0; j < array->size; j++) { + logBuffer << (int)data[j]; + + if (j + 1 < array->size) { + logBuffer << ","; + } } + logBuffer << "]\n"; + } } - logBuffer << "\n"; - - flushBuffer(); - - return success; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { - return solver->impl->getOperationStatusCode(); + return solver->impl->getOperationStatusCode(); } -char *QueryLoggingSolver::getConstraintLog(const Query& query) { +char *QueryLoggingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } void QueryLoggingSolver::setCoreSolverTimeout(double timeout) { solver->impl->setCoreSolverTimeout(timeout); } - diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index ad1722ca..bb266c67 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -1,4 +1,5 @@ -//===-- QueryLoggingSolver.h ---------------------------------------------------===// +//===-- QueryLoggingSolver.h +//---------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -8,75 +9,71 @@ //===----------------------------------------------------------------------===// #ifndef KLEE_QUERYLOGGINGSOLVER_H -#define KLEE_QUERYLOGGINGSOLVER_H +#define KLEE_QUERYLOGGINGSOLVER_H #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" -#include <fstream> -#include <sstream> using namespace klee; -/// This abstract class represents a solver that is capable of logging +/// This abstract class represents a solver that is capable of logging /// queries to a file. /// Derived classes might specialize this one by providing different formats /// for the query output. class QueryLoggingSolver : public SolverImpl { protected: - Solver *solver; - std::string ErrorInfo; - llvm::raw_fd_ostream os; - // @brief Buffer used by logBuffer - std::string BufferString; - // @brief buffer to store logs before flushing to file - llvm::raw_string_ostream logBuffer; - unsigned queryCount; - int minQueryTimeToLog; // we log to file only those queries - // which take longer than the specified time (ms); - // if this param is negative, log only those queries - // on which the solver has timed out + Solver *solver; + std::string ErrorInfo; + llvm::raw_fd_ostream os; + // @brief Buffer used by logBuffer + std::string BufferString; + // @brief buffer to store logs before flushing to file + llvm::raw_string_ostream logBuffer; + unsigned queryCount; + int minQueryTimeToLog; // we log to file only those queries + // which take longer than the specified time (ms); + // if this param is negative, log only those queries + // on which the solver has timed out - double startTime; - double lastQueryTime; - const std::string queryCommentSign; // sign representing commented lines - // in given a query format + double startTime; + double lastQueryTime; + const std::string queryCommentSign; // sign representing commented lines + // in given a query format + + virtual void startQuery(const Query &query, const char *typeName, + const Query *falseQuery = 0, + const std::vector<const Array *> *objects = 0); + + virtual void finishQuery(bool success); + + /// flushBuffer - flushes the temporary logs buffer. Depending on threshold + /// settings, contents of the buffer are either discarded or written to a + /// file. + void flushBuffer(void); + + virtual void printQuery(const Query &query, const Query *falseQuery = 0, + const std::vector<const Array *> *objects = 0) = 0; + void flushBufferConditionally(bool writeToFile); - virtual void startQuery(const Query& query, const char* typeName, - const Query* falseQuery = 0, - const std::vector<const Array*>* objects = 0); - - virtual void finishQuery(bool success); - - /// flushBuffer - flushes the temporary logs buffer. Depending on threshold - /// settings, contents of the buffer are either discarded or written to a file. - void flushBuffer(void); - - virtual void printQuery(const Query& query, - const Query* falseQuery = 0, - const std::vector<const Array*>* objects = 0) = 0; - public: - QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog); - - virtual ~QueryLoggingSolver(); + QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, int queryTimeToLog); - /// implementation of the SolverImpl interface - bool computeTruth(const Query& query, bool &isValid); - bool computeValidity(const Query& query, Solver::Validity &result); - bool computeValue(const Query& query, ref<Expr> &result); - bool computeInitialValues(const Query& query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution); - SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); -}; + virtual ~QueryLoggingSolver(); -#endif /* KLEE_QUERYLOGGINGSOLVER_H */ + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid); + bool computeValidity(const Query &query, Solver::Validity &result); + bool computeValue(const Query &query, ref<Expr> &result); + bool computeInitialValues(const Query &query, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; +#endif /* KLEE_QUERYLOGGINGSOLVER_H */ diff --git a/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery new file mode 100644 index 00000000..9116ea47 --- /dev/null +++ b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery @@ -0,0 +1,15 @@ +# RUN: %kleaver %s 2>&1 | FileCheck %s +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) 2) +(Slt 0 N0) +(Ult N1:(ReadLSB w32 0 n_args_1) 3) +(Slt 0 N1) +(Slt 1 N1) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647))) +(Ult (ReadLSB w64 56 A-data-stat) 65536) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))] +(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args]) +# CHECK: INVALID diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c_ new file mode 100644 index 00000000..88a5fca3 --- /dev/null +++ b/test/regression/2016-04-14-sdiv-2.c_ @@ -0,0 +1,25 @@ +// XFAIL: * +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log +// RUN: grep "m is 2" %t1.log + +#include <assert.h> + +int main(void) +{ + int n, m; + klee_make_symbolic(&n, sizeof n, "n"); + klee_assume(n < -1); + + if (n/2 > 0) + assert(0); + + klee_make_symbolic(&m, sizeof m, "m"); + klee_assume(m > 0); + + if (m/2 == 2) + printf("m is 2\n"); + + return 0; +} diff --git a/test/regression/lit.local.cfg b/test/regression/lit.local.cfg new file mode 100644 index 00000000..d64daf29 --- /dev/null +++ b/test/regression/lit.local.cfg @@ -0,0 +1,2 @@ +# Look for .kquery files too +config.suffixes.add('.kquery') diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index e34dd52d..80161caa 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1382,11 +1382,10 @@ int main(int argc, char **argv, char **envp) { theInterpreter = Interpreter::create(IOpts, handler); handler->setInterpreter(interpreter); - llvm::raw_ostream &infoFile = handler->getInfoStream(); for (int i=0; i<argc; i++) { - infoFile << argv[i] << (i+1<argc ? " ":"\n"); + handler->getInfoStream() << argv[i] << (i+1<argc ? " ":"\n"); } - infoFile << "PID: " << getpid() << "\n"; + handler->getInfoStream() << "PID: " << getpid() << "\n"; const Module *finalModule = interpreter->setModule(mainModule, Opts); @@ -1400,8 +1399,8 @@ int main(int argc, char **argv, char **envp) { time_t t[2]; t[0] = time(NULL); strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0])); - infoFile << buf; - infoFile.flush(); + handler->getInfoStream() << buf; + handler->getInfoStream().flush(); if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) { assert(SeedOutFile.empty()); @@ -1502,11 +1501,11 @@ int main(int argc, char **argv, char **envp) { t[1] = time(NULL); strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1])); - infoFile << buf; + handler->getInfoStream() << buf; strcpy(buf, "Elapsed: "); strcpy(format_tdiff(buf, t[1] - t[0]), "\n"); - infoFile << buf; + handler->getInfoStream() << buf; // Free all the args. for (unsigned i=0; i<InputArgv.size()+1; i++) |