about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2013-01-02 14:33:58 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2013-01-02 14:33:58 +0000
commitc7db4230beef3b81542edb5d7ae6ca606d0567dd (patch)
treef3913e6ea23e0bffbbeff0fc8f5810159c1517f9 /lib/Core
parent26bf73bf80369a24467fcf1f53165824cbcd5679 (diff)
downloadklee-c7db4230beef3b81542edb5d7ae6ca606d0567dd.tar.gz
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
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp15
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());
   }