diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-06 16:37:11 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-06 16:37:11 +0000 |
| commit | d1b298b4bd6580eeb2eec86846f8367a2132ff93 (patch) | |
| tree | cdf594b3c94d5929c2427239d61de883724857b2 /klee | |
| parent | 3867311617ba7f54764defa5e8c952dc29485b57 (diff) | |
Some documentation on query logging.
Diffstat (limited to 'klee')
| -rw-r--r-- | klee/www/Documentation.html | 2 | ||||
| -rw-r--r-- | klee/www/klee-options.html | 30 |
2 files changed, 29 insertions, 3 deletions
diff --git a/klee/www/Documentation.html b/klee/www/Documentation.html index b266e439c07..111528017ec 100644 --- a/klee/www/Documentation.html +++ b/klee/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/klee/www/klee-options.html b/klee/www/klee-options.html index 22871e0e76a..be997ec4155 100644 --- a/klee/www/klee-options.html +++ b/klee/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> |