diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-23 21:12:46 +0100 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-23 21:14:05 +0100 |
commit | 082e9d7bab796eda37624c026d8d006608625b90 (patch) | |
tree | 41583f58641fce1aa94c8ce3a0e42708aad475c2 /lib/Solver/QueryLoggingSolver.h | |
parent | a5f0334c0a844a0d6177c38375ec92ae8db217f9 (diff) | |
download | klee-082e9d7bab796eda37624c026d8d006608625b90.tar.gz |
Fix comment + Clang Formatting
Diffstat (limited to 'lib/Solver/QueryLoggingSolver.h')
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 104 |
1 files changed, 50 insertions, 54 deletions
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index ad1722ca..3068f2ab 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,70 @@ //===----------------------------------------------------------------------===// #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; - 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 */ |