From b676cabff80c1b8a7872f5263fbdadf2a1ff1148 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Fri, 11 Jan 2013 10:55:36 +0000
Subject: Documentation for klee-stats by Tomasz Kuchta.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@172190 91177308-0d34-0410-b5e6-96231b3b80d8
---
 www/Documentation.html | 14 ++++++-----
 www/klee-tools.html    | 64 ++++++++++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 70 insertions(+), 8 deletions(-)

diff --git a/www/Documentation.html b/www/Documentation.html
index 11152801..038b1f83 100644
--- a/www/Documentation.html
+++ b/www/Documentation.html
@@ -17,8 +17,7 @@
 
   <ol>
     <li>
-      <a href="Tutorials.html">KLEE Tutorials</a>: 
-
+      <a href="Tutorials.html">KLEE Tutorials</a>:
       Simple examples of how to use KLEE to test programs.
     </li>
 
@@ -28,14 +27,17 @@
     </li>
 
     <li>
-      <a href="klee-files.html">KLEE Generated Files</a>: 
-      
+      <a href="klee-files.html">KLEE Generated Files</a>:
       Overview of the main files generated by KLEE.
     </li>
 
     <li>
-      <a href="KQuery.html">KQuery Language Reference Manual</a>: 
-      
+      <a href="klee-tools.html">KLEE Tools</a>:
+      Overview of the main auxiliary tools provided by KLEE.
+    </li>
+    
+    <li>
+      <a href="KQuery.html">KQuery Language Reference Manual</a>:
       The reference manual for the KQuery language, used for interacting with
       the KLEE solver (kleaver).
     </li>
diff --git a/www/klee-tools.html b/www/klee-tools.html
index 131c1861..80ae5d35 100644
--- a/www/klee-tools.html
+++ b/www/klee-tools.html
@@ -15,10 +15,70 @@
   <h1>KLEE Tools</h1>
   <!--*********************************************************************-->
 
-  <h2>ktest-tool</h2>
+ <h3>
+  <a href="#ktest-tool">  1. ktest-tool</a> <br/>
+  <a href="#klee-stats"> 2. klee-stats</a> <br/>
+  </h3>
 
-  <h2>klee-stats</h2>
+  <h2 id="ktest-tool">ktest-tool</h2> 
 
+  <h2 id="klee-stats">klee-stats</h2>
+  <b><i>klee-stats</i></b> is a Python script used to extract and present in a
+  tabular form runtime statistics for a KLEE execution. The runtime statistics include:
+  <ul>
+    <li>The number of executed instructions</li>
+    <li>Instruction coverage in the LLVM bitcode (%)</li>
+    <li>Branch coverage in the LLVM bitcode (%)</li>
+    <li>Total static instructions in the LLVM bitcode</li>
+    <li>The number of currently active states</li>
+    <li>Megabytes of memory currently used</li>
+    <li>The number of queries issued to STP</li>
+    <li>The average number of query constructs per query</li>
+    <li>Various time statistics:
+    <ul>
+      <li>Total user time</li>
+      <li>Total wall time</li>
+      <li>Time spent in the constraint solver</li>
+      <li>Time spent in the counterexample caching code</li>
+      <li>Time spent forking</li>
+      <li>Time spent in object resolution</li>
+    </ul></li>
+  </ul>
+
+
+  <i>klee-stats</i> extracts statistics information from the <i>run.stats</i> file
+  present in the <i>klee-out-*</i> directory created during a KLEE execution.
+  The exact usage of <i>klee-stats</i> is as follows: 
+  <pre>klee-stats [options] directories</pre>
+  The <i>directories</i> parameter is a list of <i>klee-out-*</i> directories
+  created by KLEE.  A common scenario is to simply run <i>klee-stats</i> on <i>klee-last</i>.
+
+  <p>
+  In order to limit printed information only to the values of measured times, 
+  the following options can be used:
+ 
+  <ul>
+    <li><i>--print-rel-times</i>&#8212;display time values relative
+    to measured execution time</li>
+    
+    <li><i>--print-abs-times</i>&#8212;display absolute time values</li>
+  </ul>
+ 
+  The <i>--precision</i> option can be used to configure the number of fractional
+  digits displayed in floating point values. By default, 2 fractional digits
+  are displayed, but in some cases that might be not sufficient&#8212;if the value
+  is very small, e.g. 0.0001, with 2-digits precision it will be printed as 0.00.
+  </p>
+
+  <p> Various other options can be used to specify what values are
+  displayed and how they are displayed. Options for comparison of
+  statistics are also provided. More information about available
+  options can be obtained using the command:
+  <pre>klee-stats --help</pre>
+  </p>
+
+  <br/>
+  
 </div>
 </body>
 </html>
-- 
cgit 1.4.1