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.

1 files changed, 12 insertions, 1 deletions

diff --git a/klee/tools/kleaver/main.cpp b/klee/tools/kleaver/main.cpp
index 077de3edd49..16a0ea429dc 100644
--- a/klee/tools/kleaver/main.cpp
+++ b/klee/tools/kleaver/main.cpp
@@ -93,9 +93,20 @@ namespace {
   UseFastCexSolver("use-fast-cex-solver",
 		   cl::init(false));
   
+  // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different
+  // output file name used.
   cl::opt<bool>
   UseSTPQueryPCLog("use-stp-query-pc-log",
                    cl::init(false));
+   
+  // FIXME: Command line argument duplicated in Executor.cpp of Klee
+  cl::opt<unsigned 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)"));
+  
 }
 
 static std::string escapedString(const char *start, unsigned length) {
@@ -186,7 +197,7 @@ static bool EvaluateInputAST(const char *Filename,
   Solver *S, *STP = S = 
     UseDummySolver ? createDummySolver() : new STPSolver(true);
   if (UseSTPQueryPCLog)
-    S = createPCLoggingSolver(S, "stp-queries.pc");
+    S = createPCLoggingSolver(S, "stp-queries.pc", MinQueryTimeToLog);
   if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);