diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 968283b7..b8db18fe 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -164,6 +164,15 @@ namespace { cl::init(true), cl::desc("Use counterexample caching (default=on)")); + // FIXME: Command line argument duplicated in main.cpp of Kleaver + cl::opt<int> + MinQueryTimeToLog("min-query-time-to-log", + cl::init(0), + cl::value_desc("milliseconds"), + cl::desc("Set time threshold (in ms) for queries logged in files. " + "Only queries longer than threshold will be logged. (default=0). " + "Set this param to a negative value to log timeouts only.")); + cl::opt<bool> NoExternals("no-externals", cl::desc("Do not allow external function calls (default=off)")); @@ -301,7 +310,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,SOLVER_PC)) { solver = createPCLoggingSolver(solver, - baseSolverQueryPCLogPath); + baseSolverQueryPCLogPath, + MinQueryTimeToLog); klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str()); } @@ -329,7 +339,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,ALL_PC)) { solver = createPCLoggingSolver(solver, - queryPCLogPath); + queryPCLogPath, + MinQueryTimeToLog); klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str()); } |