From c7db4230beef3b81542edb5d7ae6ca606d0567dd Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 2 Jan 2013 14:33:58 +0000 Subject: Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that enables KLEE to log only the queries exceeding a certain duration, or only those that time out. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Core/Executor.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'lib/Core/Executor.cpp') 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 + 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 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()); } -- cgit 1.4.1