diff options
| -rw-r--r-- | www/Documentation.html | 14 | ||||
| -rw-r--r-- | 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>—display time values relative + to measured execution time</li> + + <li><i>--print-abs-times</i>—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—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> |