about summary refs log tree commit diff homepage
path: root/lib/Solver/QueryLoggingSolver.h
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-23 21:12:46 +0100
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-23 21:14:05 +0100
commit082e9d7bab796eda37624c026d8d006608625b90 (patch)
tree41583f58641fce1aa94c8ce3a0e42708aad475c2 /lib/Solver/QueryLoggingSolver.h
parenta5f0334c0a844a0d6177c38375ec92ae8db217f9 (diff)
downloadklee-082e9d7bab796eda37624c026d8d006608625b90.tar.gz
Fix comment + Clang Formatting
Diffstat (limited to 'lib/Solver/QueryLoggingSolver.h')
-rw-r--r--lib/Solver/QueryLoggingSolver.h104
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 */