diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/expr/Lexer.h | 2 | ||||
| -rw-r--r-- | include/expr/Parser.h | 2 | ||||
| -rw-r--r-- | include/klee/CommandLine.h | 4 | ||||
| -rw-r--r-- | include/klee/Common.h | 8 | ||||
| -rw-r--r-- | include/klee/Interpreter.h | 2 | ||||
| -rw-r--r-- | include/klee/Solver.h | 6 |
6 files changed, 12 insertions, 12 deletions
diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h index 6cce8031..9319b487 100644 --- a/include/expr/Lexer.h +++ b/include/expr/Lexer.h @@ -72,7 +72,7 @@ namespace expr { void dump(); }; - /// Lexer - Interface for lexing tokens from a .pc language file. + /// Lexer - Interface for lexing tokens from a .kquery language file. class Lexer { const char *BufferPos; /// The current lexer position. const char *BufferEnd; /// The buffer end position. diff --git a/include/expr/Parser.h b/include/expr/Parser.h index a9133e9d..fa07bae2 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -202,7 +202,7 @@ namespace expr { static bool classof(const QueryCommand *) { return true; } }; - /// Parser - Public interface for parsing a .pc language file. + /// Parser - Public interface for parsing a .kquery language file. class Parser { protected: Parser(); diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index dc69de6e..95aa51e0 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -32,9 +32,9 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType { - ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format + ALL_KQUERY, ///< Log all queries (un-optimised) in .kquery (KQuery) format ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format - SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format + SOLVER_KQUERY,///< Log queries passed to solver (optimised) in .kquery (KQuery) format SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format }; diff --git a/include/klee/Common.h b/include/klee/Common.h index 7149708a..5f0f0e1d 100644 --- a/include/klee/Common.h +++ b/include/klee/Common.h @@ -19,14 +19,14 @@ namespace klee { const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2"; const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2"; - const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc"; - const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc"; + const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery"; + const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery"; Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, - std::string queryPCLogPath, - std::string baseSolverQueryPCLogPath); + std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath); } diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index 3a4d40b4..ece84b2c 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -66,7 +66,7 @@ public: enum LogType { STP, //.CVC (STP's native language) - KQUERY, //.PC files (kQuery native language) + KQUERY, //.KQUERY files (kQuery native language) SMTLIB2 //.SMT2 files (SMTLIB version 2 files) }; diff --git a/include/klee/Solver.h b/include/klee/Solver.h index c82ab135..2f613992 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -296,9 +296,9 @@ namespace klee { /// \param s - The underlying solver to use. Solver *createIndependentSolver(Solver *s); - /// createPCLoggingSolver - Create a solver which will forward all queries - /// after writing them to the given path in .pc format. - Solver *createPCLoggingSolver(Solver *s, std::string path, + /// createKQueryLoggingSolver - Create a solver which will forward all queries + /// after writing them to the given path in .kquery format. + Solver *createKQueryLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog); /// createSMTLIBLoggingSolver - Create a solver which will forward all queries |