From 4f1d842f3b13cbdcbc44065a51365931e5ce8fe0 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Sun, 6 Jan 2013 16:37:11 +0000
Subject: Some documentation on query logging.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171657 91177308-0d34-0410-b5e6-96231b3b80d8
---
 www/Documentation.html |  2 +-
 www/klee-options.html  | 30 ++++++++++++++++++++++++++++--
 2 files changed, 29 insertions(+), 3 deletions(-)

(limited to 'www')

diff --git a/www/Documentation.html b/www/Documentation.html
index b266e439..11152801 100644
--- a/www/Documentation.html
+++ b/www/Documentation.html
@@ -24,7 +24,7 @@
 
     <li>
       <a href="klee-options.html">KLEE Options</a>:      
-      Overview of the KLEE's main command-line options.
+      Overview of KLEE's main command-line options.
     </li>
 
     <li>
diff --git a/www/klee-options.html b/www/klee-options.html
index 22871e0e..be997ec4 100644
--- a/www/klee-options.html
+++ b/www/klee-options.html
@@ -15,7 +15,12 @@
   <h1>KLEE Options</h1>
   <!--*********************************************************************-->
 
-  <h2>Search Heuristics</h2> 
+  <h3>
+  <a href="#search">  1. Search Heuristics</a> <br/>
+  <a href="#logging"> 2. Query Logging</a> <br/>
+  </h3>
+  
+  <h2 id="search">Search Heuristics</h2> 
 
   <h3>Main search heuristics</h3>
 
@@ -67,7 +72,28 @@
   <p>
     The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>.
   </p>
-    
+  
+  <h2 id="logging">Query Logging</h2> 
+
+  To log the queries issued by KLEE during symbolic execution, you can use the following options:
+  <ol>
+    <li>
+    <b>--use-query-log=TYPE:FORMAT</b>, where:
+    <ul>
+      <li><b>TYPE</b> is either <b>all</b> to log all the queries KLEE made during execution before any optimisation (e.g. caching, constraint independence) is performed, or <b>solver</b> to log only the queries passed to KLEE's underlying solver.  Note that it is possible that some of the unoptimized queries are never executed  or are modified before being executed by KLEE's underlying solver.</li>
+      <li><b>FORMAT</b> is the format in which queries are logged and can be either <b>pc</b> for the <a href="KQuery.html">KQuery</a> format, or <b>smt2</b> for the <a href="http://www.smtlib.org">SMT-LIBv2</a> format. 
+    </ul>
+    <li>
+    <b>--min-query-time-to-log=TIME</b> (in ms) is used to log only queries that exceed a certain time limit.  <b>TIME</b> can be:
+    <ul>
+      <li><b>0</b> (default): to log all queries</li>
+      <li><b><0</b>: a negative value specifies that only queries that timed out should be logged.  The timeout value is specified via the <b>--max-stp-time</b> option.</li>
+      <li><b>>0</b>: only queries that took more that <b>TIME</b> milliseconds should be logged.
+    </ul>
+    </li>
+  </li>
+  </ol>
+  
 </div>
 </body>
 </html>
-- 
cgit 1.4.1